defpred S1[ set ] means ( ( for s being stack of F1() st emp s holds
[s,F4()] in $1 ) & ( for s being stack of F1()
for a being Element of F1()
for v being Element of F3() st [s,v] in $1 holds
[(push (a,s)),F5(a,v)] in $1 ) );
consider M being set such that
A1: for x being set holds
( x in M iff ( x in bool [: the carrier' of F1(),F3():] & S1[x] ) ) from XBOOLE_0:sch 1();
 B1: ( S1[[: the carrier' of F1(),F3():]] & [: the carrier' of F1(),F3():] in bool [: the carrier' of F1(),F3():] ) by ZFMISC_1:def 1;
then A2: [: the carrier' of F1(),F3():] in M by A1;
reconsider M = M as non empty set by A1, B1;
set F = meet M;
reconsider F = meet M as Subset of [: the carrier' of F1(),F3():] by A2, SETFAM_1:3;
defpred S2[ stack of F1()] means for y1, y2 being set st [$1,y1] in F & [$1,y2] in F holds
y1 = y2;
A8: S1[F]
proof
hereby :: thesis: for s being stack of F1()
for a being Element of F1()
for v being Element of F3() st [s,v] in F holds
[(push (a,s)),F5(a,v)] in F
let s be stack of F1(); :: thesis: ( emp s implies [s,F4()] in F )
assume emp s ; :: thesis: [s,F4()] in F
then for Y being set st Y in M holds
[s,F4()] in Y by A1;
hence [s,F4()] in F by SETFAM_1:def 1; :: thesis: verum
end;
let s be stack of F1(); :: thesis: for a being Element of F1()
for v being Element of F3() st [s,v] in F holds
[(push (a,s)),F5(a,v)] in F
let a be Element of F1(); :: thesis: for v being Element of F3() st [s,v] in F holds
[(push (a,s)),F5(a,v)] in F
let v be Element of F3(); :: thesis: ( [s,v] in F implies [(push (a,s)),F5(a,v)] in F )
assume S1: [s,v] in F ; :: thesis: [(push (a,s)),F5(a,v)] in F
now
let Y be set ; :: thesis: ( Y in M implies [(push (a,s)),F5(a,v)] in Y )
assume Y in M ; :: thesis: [(push (a,s)),F5(a,v)] in Y
then ( S1[Y] & [s,v] in Y ) by S1, A1, SETFAM_1:def 1;
hence [(push (a,s)),F5(a,v)] in Y ; :: thesis: verum
end;
hence [(push (a,s)),F5(a,v)] in F by SETFAM_1:def 1; :: thesis: verum
end;
defpred S3[ stack of F1()] means ex y being set st [$1,y] in F;
A6: for s being stack of F1() st emp s holds
S3[s]
proof
let s be stack of F1(); :: thesis: ( emp s implies S3[s] )
assume Z0: emp s ; :: thesis: S3[s]
take y = F4(); :: thesis: [s,y] in F
for Y being set st Y in M holds
[s,F4()] in Y by Z0, A1;
hence [s,y] in F by SETFAM_1:def 1; :: thesis: verum
end;
A7: for s being stack of F1()
for e being Element of F1() st S3[s] holds
S3[ push (e,s)]
proof
let s be stack of F1(); :: thesis: for e being Element of F1() st S3[s] holds
S3[ push (e,s)]
let e be Element of F1(); :: thesis: ( S3[s] implies S3[ push (e,s)] )
given y being set such that M1: [s,y] in F ; :: thesis: S3[ push (e,s)]
reconsider y = y as Element of F3() by M1, ZFMISC_1:87;
take z = F5(e,y); :: thesis: [(push (e,s)),z] in F
now
let Y be set ; :: thesis: ( Y in M implies [(push (e,s)),z] in Y )
assume M2: Y in M ; :: thesis: [(push (e,s)),z] in Y
then [s,y] in Y by M1, SETFAM_1:def 1;
hence [(push (e,s)),z] in Y by M2, A1; :: thesis: verum
end;
hence [(push (e,s)),z] in F by SETFAM_1:def 1; :: thesis: verum
end;
A3: for s being stack of F1() st emp s holds
S2[s]
proof
let s be stack of F1(); :: thesis: ( emp s implies S2[s] )
assume B1: emp s ; :: thesis: S2[s]
let y1, y2 be set ; :: thesis: ( [s,y1] in F & [s,y2] in F implies y1 = y2 )
assume B2: ( [s,y1] in F & [s,y2] in F ) ; :: thesis: y1 = y2
set Y1 = F \ {[s,y1]};
set Y2 = F \ {[s,y2]};
B8: now
assume B4: y1 <> F4() ; :: thesis: contradiction
S1[F \ {[s,y1]}]
proof
hereby :: thesis: for s being stack of F1()
for a being Element of F1()
for v being Element of F3() st [s,v] in F \ {[s,y1]} holds
[(push (a,s)),F5(a,v)] in F \ {[s,y1]}
let s1 be stack of F1(); :: thesis: ( emp s1 implies [s1,F4()] in F \ {[s,y1]} )
assume emp s1 ; :: thesis: [s1,F4()] in F \ {[s,y1]}
then B5: [s1,F4()] in F by A8;
[s,y1] <> [s1,F4()] by B4, ZFMISC_1:27;
then [s1,F4()] nin {[s,y1]} by TARSKI:def 1;
hence [s1,F4()] in F \ {[s,y1]} by B5, XBOOLE_0:def 5; :: thesis: verum
end;
let s1 be stack of F1(); :: thesis: for a being Element of F1()
for v being Element of F3() st [s1,v] in F \ {[s,y1]} holds
[(push (a,s1)),F5(a,v)] in F \ {[s,y1]}
let a be Element of F1(); :: thesis: for v being Element of F3() st [s1,v] in F \ {[s,y1]} holds
[(push (a,s1)),F5(a,v)] in F \ {[s,y1]}
let v be Element of F3(); :: thesis: ( [s1,v] in F \ {[s,y1]} implies [(push (a,s1)),F5(a,v)] in F \ {[s,y1]} )
assume [s1,v] in F \ {[s,y1]} ; :: thesis: [(push (a,s1)),F5(a,v)] in F \ {[s,y1]}
then [s1,v] in F by XBOOLE_0:def 5;
then B6: [(push (a,s1)),F5(a,v)] in F by A8;
push (a,s1) <> s by B1, PUSHNE;
then [s,y1] <> [(push (a,s1)),F5(a,v)] by ZFMISC_1:27;
then [(push (a,s1)),F5(a,v)] nin {[s,y1]} by TARSKI:def 1;
hence [(push (a,s1)),F5(a,v)] in F \ {[s,y1]} by B6, XBOOLE_0:def 5; :: thesis: verum
end;
then F \ {[s,y1]} in M by A1;
then F c= F \ {[s,y1]} by SETFAM_1:3;
then ( [s,y1] in F \ {[s,y1]} & [s,y1] in {[s,y1]} ) by B2, TARSKI:def 1;
hence contradiction by XBOOLE_0:def 5; :: thesis: verum
end;
now
assume B4: y2 <> F4() ; :: thesis: contradiction
S1[F \ {[s,y2]}]
proof
hereby :: thesis: for s being stack of F1()
for a being Element of F1()
for v being Element of F3() st [s,v] in F \ {[s,y2]} holds
[(push (a,s)),F5(a,v)] in F \ {[s,y2]}
let s1 be stack of F1(); :: thesis: ( emp s1 implies [s1,F4()] in F \ {[s,y2]} )
assume emp s1 ; :: thesis: [s1,F4()] in F \ {[s,y2]}
then B5: [s1,F4()] in F by A8;
[s,y2] <> [s1,F4()] by B4, ZFMISC_1:27;
then [s1,F4()] nin {[s,y2]} by TARSKI:def 1;
hence [s1,F4()] in F \ {[s,y2]} by B5, XBOOLE_0:def 5; :: thesis: verum
end;
let s1 be stack of F1(); :: thesis: for a being Element of F1()
for v being Element of F3() st [s1,v] in F \ {[s,y2]} holds
[(push (a,s1)),F5(a,v)] in F \ {[s,y2]}
let a be Element of F1(); :: thesis: for v being Element of F3() st [s1,v] in F \ {[s,y2]} holds
[(push (a,s1)),F5(a,v)] in F \ {[s,y2]}
let v be Element of F3(); :: thesis: ( [s1,v] in F \ {[s,y2]} implies [(push (a,s1)),F5(a,v)] in F \ {[s,y2]} )
assume [s1,v] in F \ {[s,y2]} ; :: thesis: [(push (a,s1)),F5(a,v)] in F \ {[s,y2]}
then [s1,v] in F by XBOOLE_0:def 5;
then B6: [(push (a,s1)),F5(a,v)] in F by A8;
push (a,s1) <> s by B1, PUSHNE;
then [s,y2] <> [(push (a,s1)),F5(a,v)] by ZFMISC_1:27;
then [(push (a,s1)),F5(a,v)] nin {[s,y2]} by TARSKI:def 1;
hence [(push (a,s1)),F5(a,v)] in F \ {[s,y2]} by B6, XBOOLE_0:def 5; :: thesis: verum
end;
then F \ {[s,y2]} in M by A1;
then F c= F \ {[s,y2]} by SETFAM_1:3;
then ( [s,y2] in F \ {[s,y2]} & [s,y2] in {[s,y2]} ) by B2, TARSKI:def 1;
hence contradiction by XBOOLE_0:def 5; :: thesis: verum
end;
hence y1 = y2 by B8; :: thesis: verum
end;
A4: for s being stack of F1()
for e being Element of F1() st S2[s] holds
S2[ push (e,s)]
proof
let s be stack of F1(); :: thesis: for e being Element of F1() st S2[s] holds
S2[ push (e,s)]
let e be Element of F1(); :: thesis: ( S2[s] implies S2[ push (e,s)] )
assume C1: S2[s] ; :: thesis: S2[ push (e,s)]
let y1, y2 be set ; :: thesis: ( [(push (e,s)),y1] in F & [(push (e,s)),y2] in F implies y1 = y2 )
assume C2: ( [(push (e,s)),y1] in F & [(push (e,s)),y2] in F ) ; :: thesis: y1 = y2
S3[s] from STACKS_1:sch 3(A6, A7);
then consider y being set such that
C9: [s,y] in F ;
reconsider y = y as Element of F3() by C9, ZFMISC_1:87;
set Y1 = F \ {[(push (e,s)),y1]};
set Y2 = F \ {[(push (e,s)),y2]};
C8: now
assume C4: y1 <> F5(e,y) ; :: thesis: contradiction
S1[F \ {[(push (e,s)),y1]}]
proof
hereby :: thesis: for s being stack of F1()
for a being Element of F1()
for v being Element of F3() st [s,v] in F \ {[(push (e,s)),y1]} holds
[(push (a,s)),F5(a,v)] in F \ {[(push (e,s)),y1]}
let s1 be stack of F1(); :: thesis: ( emp s1 implies [s1,F4()] in F \ {[(push (e,s)),y1]} )
assume C11: emp s1 ; :: thesis: [s1,F4()] in F \ {[(push (e,s)),y1]}
then C5: [s1,F4()] in F by A8;
not emp push (e,s) by PUSHNE;
then [(push (e,s)),y1] <> [s1,F4()] by C11, ZFMISC_1:27;
then [s1,F4()] nin {[(push (e,s)),y1]} by TARSKI:def 1;
hence [s1,F4()] in F \ {[(push (e,s)),y1]} by C5, XBOOLE_0:def 5; :: thesis: verum
end;
let s1 be stack of F1(); :: thesis: for a being Element of F1()
for v being Element of F3() st [s1,v] in F \ {[(push (e,s)),y1]} holds
[(push (a,s1)),F5(a,v)] in F \ {[(push (e,s)),y1]}
let a be Element of F1(); :: thesis: for v being Element of F3() st [s1,v] in F \ {[(push (e,s)),y1]} holds
[(push (a,s1)),F5(a,v)] in F \ {[(push (e,s)),y1]}
let v be Element of F3(); :: thesis: ( [s1,v] in F \ {[(push (e,s)),y1]} implies [(push (a,s1)),F5(a,v)] in F \ {[(push (e,s)),y1]} )
assume [s1,v] in F \ {[(push (e,s)),y1]} ; :: thesis: [(push (a,s1)),F5(a,v)] in F \ {[(push (e,s)),y1]}
then C10: [s1,v] in F by XBOOLE_0:def 5;
then C6: [(push (a,s1)),F5(a,v)] in F by A8;
now
assume [(push (e,s)),y1] = [(push (a,s1)),F5(a,v)] ; :: thesis: contradiction
then C12: ( push (e,s) = push (a,s1) & y1 = F5(a,v) ) by ZFMISC_1:27;
then ( e = a & s = s1 ) by Th2;
hence contradiction by C1, C9, C10, C4, C12; :: thesis: verum
end;
then [(push (a,s1)),F5(a,v)] nin {[(push (e,s)),y1]} by TARSKI:def 1;
hence [(push (a,s1)),F5(a,v)] in F \ {[(push (e,s)),y1]} by C6, XBOOLE_0:def 5; :: thesis: verum
end;
then F \ {[(push (e,s)),y1]} in M by A1;
then F c= F \ {[(push (e,s)),y1]} by SETFAM_1:3;
then ( [(push (e,s)),y1] in F \ {[(push (e,s)),y1]} & [(push (e,s)),y1] in {[(push (e,s)),y1]} ) by C2, TARSKI:def 1;
hence contradiction by XBOOLE_0:def 5; :: thesis: verum
end;
now
assume C4: y2 <> F5(e,y) ; :: thesis: contradiction
S1[F \ {[(push (e,s)),y2]}]
proof
hereby :: thesis: for s being stack of F1()
for a being Element of F1()
for v being Element of F3() st [s,v] in F \ {[(push (e,s)),y2]} holds
[(push (a,s)),F5(a,v)] in F \ {[(push (e,s)),y2]}
let s1 be stack of F1(); :: thesis: ( emp s1 implies [s1,F4()] in F \ {[(push (e,s)),y2]} )
assume C11: emp s1 ; :: thesis: [s1,F4()] in F \ {[(push (e,s)),y2]}
then C5: [s1,F4()] in F by A8;
not emp push (e,s) by PUSHNE;
then [(push (e,s)),y2] <> [s1,F4()] by C11, ZFMISC_1:27;
then [s1,F4()] nin {[(push (e,s)),y2]} by TARSKI:def 1;
hence [s1,F4()] in F \ {[(push (e,s)),y2]} by C5, XBOOLE_0:def 5; :: thesis: verum
end;
let s1 be stack of F1(); :: thesis: for a being Element of F1()
for v being Element of F3() st [s1,v] in F \ {[(push (e,s)),y2]} holds
[(push (a,s1)),F5(a,v)] in F \ {[(push (e,s)),y2]}
let a be Element of F1(); :: thesis: for v being Element of F3() st [s1,v] in F \ {[(push (e,s)),y2]} holds
[(push (a,s1)),F5(a,v)] in F \ {[(push (e,s)),y2]}
let v be Element of F3(); :: thesis: ( [s1,v] in F \ {[(push (e,s)),y2]} implies [(push (a,s1)),F5(a,v)] in F \ {[(push (e,s)),y2]} )
assume [s1,v] in F \ {[(push (e,s)),y2]} ; :: thesis: [(push (a,s1)),F5(a,v)] in F \ {[(push (e,s)),y2]}
then C10: [s1,v] in F by XBOOLE_0:def 5;
then C6: [(push (a,s1)),F5(a,v)] in F by A8;
now
assume [(push (e,s)),y2] = [(push (a,s1)),F5(a,v)] ; :: thesis: contradiction
then C12: ( push (e,s) = push (a,s1) & y2 = F5(a,v) ) by ZFMISC_1:27;
then ( e = a & s = s1 ) by Th2;
hence contradiction by C1, C9, C10, C4, C12; :: thesis: verum
end;
then [(push (a,s1)),F5(a,v)] nin {[(push (e,s)),y2]} by TARSKI:def 1;
hence [(push (a,s1)),F5(a,v)] in F \ {[(push (e,s)),y2]} by C6, XBOOLE_0:def 5; :: thesis: verum
end;
then F \ {[(push (e,s)),y2]} in M by A1;
then F c= F \ {[(push (e,s)),y2]} by SETFAM_1:3;
then ( [(push (e,s)),y2] in F \ {[(push (e,s)),y2]} & [(push (e,s)),y2] in {[(push (e,s)),y2]} ) by C2, TARSKI:def 1;
hence contradiction by XBOOLE_0:def 5; :: thesis: verum
end;
hence y1 = y2 by C8; :: thesis: verum
end;
A5: F is Function-like
proof
let x, y1, y2 be set ; :: according to FUNCT_1:def 1 :: thesis: ( not [x,y1] in F or not [x,y2] in F or y1 = y2 )
assume B1: ( [x,y1] in F & [x,y2] in F ) ; :: thesis: y1 = y2
then reconsider x = x as stack of F1() by ZFMISC_1:87;
S2[x] from STACKS_1:sch 3(A3, A4);
hence y1 = y2 by B1; :: thesis: verum
end;
F is quasi_total
proof
per cases not ( F3() = {} & not the carrier' of F1() = {} & not ( F3() = {} & the carrier' of F1() <> {} ) ) ;
:: according to FUNCT_2:def 1
case ( F3() = {} implies the carrier' of F1() = {} ) ; :: thesis: the carrier' of F1() = dom F
thus the carrier' of F1() c= dom F :: according to XBOOLE_0:def 10 :: thesis: dom F c= the carrier' of F1()
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier' of F1() or x in dom F )
assume x in the carrier' of F1() ; :: thesis: x in dom F
then reconsider x = x as stack of F1() ;
S3[x] from STACKS_1:sch 3(A6, A7);
hence x in dom F by RELAT_1:def 4; :: thesis: verum
end;
thus dom F c= the carrier' of F1() ; :: thesis: verum
end;
case ( F3() = {} & the carrier' of F1() <> {} ) ; :: thesis: F = {}
hence F = {} ; :: thesis: verum
end;
end;
end;
then reconsider F = F as Function of the carrier' of F1(),F3() by A5;
take a = F . F2(); :: thesis: ex F being Function of the carrier' of F1(),F3() st
( a = F . F2() & ( for s1 being stack of F1() st emp s1 holds
F . s1 = F4() ) & ( for s1 being stack of F1()
for e being Element of F1() holds F . (push (e,s1)) = F5(e,(F . s1)) ) )
take F ; :: thesis: ( a = F . F2() & ( for s1 being stack of F1() st emp s1 holds
F . s1 = F4() ) & ( for s1 being stack of F1()
for e being Element of F1() holds F . (push (e,s1)) = F5(e,(F . s1)) ) )
thus a = F . F2() ; :: thesis: ( ( for s1 being stack of F1() st emp s1 holds
F . s1 = F4() ) & ( for s1 being stack of F1()
for e being Element of F1() holds F . (push (e,s1)) = F5(e,(F . s1)) ) )
hereby :: thesis: for s1 being stack of F1()
for e being Element of F1() holds F . (push (e,s1)) = F5(e,(F . s1))
let s1 be stack of F1(); :: thesis: ( emp s1 implies F . s1 = F4() )
assume emp s1 ; :: thesis: F . s1 = F4()
then [s1,F4()] in F by A8;
hence F . s1 = F4() by FUNCT_1:1; :: thesis: verum
end;
let s1 be stack of F1(); :: thesis: for e being Element of F1() holds F . (push (e,s1)) = F5(e,(F . s1))
let e be Element of F1(); :: thesis: F . (push (e,s1)) = F5(e,(F . s1))
dom F = the carrier' of F1() by FUNCT_2:def 1;
then [s1,(F . s1)] in F by FUNCT_1:def 2;
then [(push (e,s1)),F5(e,(F . s1))] in F by A8;
hence F . (push (e,s1)) = F5(e,(F . s1)) by FUNCT_1:1; :: thesis: verum