set T = bool (Subformulae v);
set Y = [:(bool (Subformulae v)),(bool (Subformulae v)),(bool (Subformulae v)):];
defpred S1[ set , set ] means ( $1 in [:(bool (Subformulae v)),(bool (Subformulae v)),(bool (Subformulae v)):] & ex y1, y2, y3 being Subset of (Subformulae v) ex N being strict LTLnode of v st
( $1 = [[y1,y2],y3] & $2 = N & the LTLold of N = y1 & the LTLnew of N = y2 & the LTLnext of N = y3 ) );
A1:
for x, y, z being set st S1[x,y] & S1[x,z] holds
y = z
proof
let x,
y,
z be
set ;
:: thesis: ( S1[x,y] & S1[x,z] implies y = z )
assume that B1:
S1[
x,
y]
and B2:
S1[
x,
z]
;
:: thesis: y = z
consider y1,
y2,
y3 being
Subset of
(Subformulae v),
N1 being
strict LTLnode of
v such that B3:
(
x = [[y1,y2],y3] &
y = N1 & the
LTLold of
N1 = y1 & the
LTLnew of
N1 = y2 & the
LTLnext of
N1 = y3 )
by B1;
consider z1,
z2,
z3 being
Subset of
(Subformulae v),
N2 being
strict LTLnode of
v such that B4:
(
x = [[z1,z2],z3] &
z = N2 & the
LTLold of
N2 = z1 & the
LTLnew of
N2 = z2 & the
LTLnext of
N2 = z3 )
by B2;
(
[y1,y2] = [z1,z2] &
y3 = z3 )
by B3, B4, ZFMISC_1:33;
then
(
y1 = z1 &
y2 = z2 &
y3 = z3 )
by ZFMISC_1:33;
hence
y = z
by B3, B4;
:: thesis: verum
end;
consider IT being set such that
A2:
for x being set holds
( x in IT iff ex y being set st
( y in [:(bool (Subformulae v)),(bool (Subformulae v)),(bool (Subformulae v)):] & S1[y,x] ) )
from TARSKI:sch 1(A1);
not IT is empty
proof
set e =
{} v;
set x =
LTLnode(#
({} v),
({} v),
({} v) #);
set y =
[[({} v),({} v)],({} v)];
[({} v),({} v)] in [:(bool (Subformulae v)),(bool (Subformulae v)):]
by ZFMISC_1:def 2;
then
[[({} v),({} v)],({} v)] in [:[:(bool (Subformulae v)),(bool (Subformulae v)):],(bool (Subformulae v)):]
by ZFMISC_1:def 2;
then
S1[
[[({} v),({} v)],({} v)],
LTLnode(#
({} v),
({} v),
({} v) #)]
by ZFMISC_1:def 3;
hence
not
IT is
empty
by A2;
:: thesis: verum
end;
then reconsider IT = IT as non empty set ;
take
IT
; :: thesis: for x being set holds
( x in IT iff ex N being strict LTLnode of v st x = N )
A3:
for x being set st x in IT holds
ex N being strict LTLnode of v st x = N
for x being set st ex N being strict LTLnode of v st x = N holds
x in IT
proof
let x be
set ;
:: thesis: ( ex N being strict LTLnode of v st x = N implies x in IT )
assume
ex
N being
strict LTLnode of
v st
x = N
;
:: thesis: x in IT
then consider N being
strict LTLnode of
v such that B1:
x = N
;
set y1 = the
LTLold of
N;
set y2 = the
LTLnew of
N;
set y3 = the
LTLnext of
N;
set y =
[[the LTLold of N,the LTLnew of N],the LTLnext of N];
[the LTLold of N,the LTLnew of N] in [:(bool (Subformulae v)),(bool (Subformulae v)):]
by ZFMISC_1:def 2;
then
[[the LTLold of N,the LTLnew of N],the LTLnext of N] in [:[:(bool (Subformulae v)),(bool (Subformulae v)):],(bool (Subformulae v)):]
by ZFMISC_1:def 2;
then
[[the LTLold of N,the LTLnew of N],the LTLnext of N] in [:(bool (Subformulae v)),(bool (Subformulae v)),(bool (Subformulae v)):]
by ZFMISC_1:def 3;
hence
x in IT
by B1, A2;
:: thesis: verum
end;
hence
for x being set holds
( x in IT iff ex N being strict LTLnode of v st x = N )
by A3; :: thesis: verum