set T = bool (Subformulae v);
set Y = [:(bool (Subformulae v)),(bool (Subformulae v)),(bool (Subformulae v)):];
defpred S1[ object , object ] 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 over 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 object st S1[x,y] & S1[x,z] holds
y = z
proof
let x,
y,
z be
object ;
( S1[x,y] & S1[x,z] implies y = z )
assume that A2:
S1[
x,
y]
and A3:
S1[
x,
z]
;
y = z
consider y1,
y2,
y3 being
Subset of
(Subformulae v),
N1 being
strict LTLnode over
v such that A4:
x = [[y1,y2],y3]
and A5:
(
y = N1 & the
LTLold of
N1 = y1 & the
LTLnew of
N1 = y2 & the
LTLnext of
N1 = y3 )
by A2;
consider z1,
z2,
z3 being
Subset of
(Subformulae v),
N2 being
strict LTLnode over
v such that A6:
x = [[z1,z2],z3]
and A7:
(
z = N2 & the
LTLold of
N2 = z1 & the
LTLnew of
N2 = z2 & the
LTLnext of
N2 = z3 )
by A3;
A8:
y3 = z3
by A4, A6, XTUPLE_0:1;
A9:
[y1,y2] = [z1,z2]
by A4, A6, XTUPLE_0:1;
then
y1 = z1
by XTUPLE_0:1;
hence
y = z
by A5, A7, A9, A8, XTUPLE_0:1;
verum
end;
consider IT being set such that
A10:
for x being object holds
( x in IT iff ex y being object 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 A10;
verum
end;
then reconsider IT = IT as non empty set ;
A11:
for x being object st ex N being strict LTLnode over v st x = N holds
x in IT
proof
let x be
object ;
( ex N being strict LTLnode over v st x = N implies x in IT )
assume
ex
N being
strict LTLnode over
v st
x = N
;
x in IT
then consider N being
strict LTLnode over
v such that A12:
x = N
;
set y3 = the
LTLnext of
N;
set y2 = the
LTLnew of
N;
set y1 = the
LTLold 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 A10, A12;
verum
end;
take
IT
; for x being object holds
( x in IT iff ex N being strict LTLnode over v st x = N )
for x being object st x in IT holds
ex N being strict LTLnode over v st x = N
hence
for x being object holds
( x in IT iff ex N being strict LTLnode over v st x = N )
by A11; verum