let W be Universe; :: thesis: for L being DOMAIN-Sequence of st omega in W & ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Union (L | a) ) holds
for H being ZF-formula ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) )
let L be DOMAIN-Sequence of ; :: thesis: ( omega in W & ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Union (L | a) ) implies for H being ZF-formula ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) ) )
assume A1: ( omega in W & ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Union (L | a) ) ) ; :: thesis: for H being ZF-formula ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) )
set M = Union L;
A2: dom L = On W by Def5;
A3: union (rng L) = Union L by CARD_3:def 4;
defpred S1[ ZF-formula] means ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= $1 iff L . a,f |= $1 ) ) );
A4: for H being ZF-formula st H is atomic holds
S1[H]
proof
let H be ZF-formula; :: thesis: ( H is atomic implies S1[H] )
assume A5: ( H is being_equality or H is being_membership ) ; :: according to ZF_LANG:def 15 :: thesis: S1[H]
A6: ( dom (id (On W)) = On W & rng (id (On W)) = On W ) by RELAT_1:71;
then reconsider phi = id (On W) as T-Sequence by ORDINAL1:def 7;
reconsider phi = phi as Ordinal-Sequence by A6, ORDINAL2:def 8;
reconsider phi = phi as Ordinal-Sequence of W by A6, RELSET_1:11, FUNCT_2:def 1;
take phi ; :: thesis: ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) )
thus A7: phi is increasing :: thesis: ( phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) )
proof
let A be Ordinal; :: according to ORDINAL2:def 16 :: thesis: for b1 being set holds
( not A in b1 or not b1 in dom phi or phi . A in phi . b1 )
let B be Ordinal; :: thesis: ( not A in B or not B in dom phi or phi . A in phi . B )
assume A8: ( A in B & B in dom phi ) ; :: thesis: phi . A in phi . B
then ( phi . A = A & phi . B = B ) by FUNCT_1:35, ORDINAL1:19;
hence phi . A in phi . B by A8; :: thesis: verum
end;
thus phi is continuous :: thesis: for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H )
proof
let A be Ordinal; :: according to ORDINAL2:def 17 :: thesis: for b1 being set holds
( not A in dom phi or A = {} or not A is limit_ordinal or not b1 = phi . A or b1 is_limes_of phi | A )
let B be Ordinal; :: thesis: ( not A in dom phi or A = {} or not A is limit_ordinal or not B = phi . A or B is_limes_of phi | A )
assume A9: ( A in dom phi & A <> {} & A is limit_ordinal & B = phi . A ) ; :: thesis: B is_limes_of phi | A
then A10: ( phi . A = A & A c= dom phi ) by FUNCT_1:35, ORDINAL1:def 2;
phi | A = phi * (id A) by RELAT_1:94
.= id ((dom phi) /\ A) by A6, FUNCT_1:43
.= id A by A10, XBOOLE_1:28 ;
then rng (phi | A) = A by RELAT_1:71;
then A11: sup (phi | A) = B by A9, A10, ORDINAL2:26;
( dom (phi | A) = A & phi | A is increasing ) by A7, A10, ORDINAL4:15, RELAT_1:91;
hence B is_limes_of phi | A by A9, A11, ORDINAL4:8; :: thesis: verum
end;
let a be Ordinal of W; :: thesis: ( phi . a = a & {} <> a implies for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) )
assume ( phi . a = a & {} <> a ) ; :: thesis: for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H )
let f be Function of VAR ,(L . a); :: thesis: ( Union L,(Union L) ! f |= H iff L . a,f |= H )
thus ( Union L,(Union L) ! f |= H implies L . a,f |= H ) :: thesis: ( L . a,f |= H implies Union L,(Union L) ! f |= H )
proof
assume A12: Union L,(Union L) ! f |= H ; :: thesis: L . a,f |= H
A13: (Union L) ! f = f by Th24, ZF_LANG1:def 2;
A14: now
assume H is being_equality ; :: thesis: L . a,f |= H
then A15: H = (Var1 H) '=' (Var2 H) by ZF_LANG:53;
then ((Union L) ! f) . (Var1 H) = ((Union L) ! f) . (Var2 H) by A12, ZF_MODEL:12;
hence L . a,f |= H by A13, A15, ZF_MODEL:12; :: thesis: verum
end;
hence L . a,f |= H by A5, A14; :: thesis: verum
end;
assume A17: L . a,f |= H ; :: thesis: Union L,(Union L) ! f |= H
A18: (Union L) ! f = f by Th24, ZF_LANG1:def 2;
A19: now
assume H is being_equality ; :: thesis: Union L,(Union L) ! f |= H
then A20: H = (Var1 H) '=' (Var2 H) by ZF_LANG:53;
then f . (Var1 H) = f . (Var2 H) by A17, ZF_MODEL:12;
hence Union L,(Union L) ! f |= H by A18, A20, ZF_MODEL:12; :: thesis: verum
end;
now
assume H is being_membership ; :: thesis: Union L,(Union L) ! f |= H
then A21: H = (Var1 H) 'in' (Var2 H) by ZF_LANG:54;
then f . (Var1 H) in f . (Var2 H) by A17, ZF_MODEL:13;
hence Union L,(Union L) ! f |= H by A18, A21, ZF_MODEL:13; :: thesis: verum
end;
hence Union L,(Union L) ! f |= H by A5, A19; :: thesis: verum
end;
A22: for H being ZF-formula st H is negative & S1[ the_argument_of H] holds
S1[H]
proof
let H be ZF-formula; :: thesis: ( H is negative & S1[ the_argument_of H] implies S1[H] )
assume H is negative ; :: thesis: ( not S1[ the_argument_of H] or S1[H] )
then A23: H = 'not' (the_argument_of H) by ZF_LANG:def 30;
given phi being Ordinal-Sequence of W such that A24: ( phi is increasing & phi is continuous ) and
A25: for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= the_argument_of H iff L . a,f |= the_argument_of H ) ; :: thesis: S1[H]
take phi ; :: thesis: ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) )
thus ( phi is increasing & phi is continuous ) by A24; :: thesis: for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H )
let a be Ordinal of W; :: thesis: ( phi . a = a & {} <> a implies for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) )
assume A26: ( phi . a = a & {} <> a ) ; :: thesis: for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H )
A27: L . a c= Union L by Th24;
let f be Function of VAR ,(L . a); :: thesis: ( Union L,(Union L) ! f |= H iff L . a,f |= H )
thus ( Union L,(Union L) ! f |= H implies L . a,f |= H ) :: thesis: ( L . a,f |= H implies Union L,(Union L) ! f |= H )
proof
assume Union L,(Union L) ! f |= H ; :: thesis: L . a,f |= H
then ( not Union L,(Union L) ! f |= the_argument_of H & f = (Union L) ! f ) by A23, A27, ZF_LANG1:def 2, ZF_MODEL:14;
then not L . a,f |= the_argument_of H by A25, A26;
hence L . a,f |= H by A23, ZF_MODEL:14; :: thesis: verum
end;
assume L . a,f |= H ; :: thesis: Union L,(Union L) ! f |= H
then not L . a,f |= the_argument_of H by A23, ZF_MODEL:14;
then not Union L,(Union L) ! f |= the_argument_of H by A25, A26;
hence Union L,(Union L) ! f |= H by A23, ZF_MODEL:14; :: thesis: verum
end;
A28: for H being ZF-formula st H is conjunctive & S1[ the_left_argument_of H] & S1[ the_right_argument_of H] holds
S1[H]
proof
let H be ZF-formula; :: thesis: ( H is conjunctive & S1[ the_left_argument_of H] & S1[ the_right_argument_of H] implies S1[H] )
assume H is conjunctive ; :: thesis: ( not S1[ the_left_argument_of H] or not S1[ the_right_argument_of H] or S1[H] )
then A29: H = (the_left_argument_of H) '&' (the_right_argument_of H) by ZF_LANG:58;
given fi1 being Ordinal-Sequence of W such that A30: ( fi1 is increasing & fi1 is continuous ) and
A31: for a being Ordinal of W st fi1 . a = a & {} <> a holds
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= the_left_argument_of H iff L . a,f |= the_left_argument_of H ) ; :: thesis: ( not S1[ the_right_argument_of H] or S1[H] )
given fi2 being Ordinal-Sequence of W such that A32: ( fi2 is increasing & fi2 is continuous ) and
A33: for a being Ordinal of W st fi2 . a = a & {} <> a holds
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= the_right_argument_of H iff L . a,f |= the_right_argument_of H ) ; :: thesis: S1[H]
take phi = fi2 * fi1; :: thesis: ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) )
ex fi being Ordinal-Sequence st
( fi = fi2 * fi1 & fi is increasing ) by A30, A32, ORDINAL4:13;
hence ( phi is increasing & phi is continuous ) by A30, A32, ORDINAL4:17; :: thesis: for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H )
let a be Ordinal of W; :: thesis: ( phi . a = a & {} <> a implies for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) )
assume A34: ( phi . a = a & {} <> a ) ; :: thesis: for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H )
A35: ( a in dom fi1 & a in dom fi2 & a in dom phi ) by ORDINAL4:36;
then A36: ( a c= fi1 . a & a c= fi2 . a ) by A30, A32, ORDINAL4:10;
A37: now
assume fi1 . a <> a ; :: thesis: contradiction
then a c< fi1 . a by A36, XBOOLE_0:def 8;
then A38: a in fi1 . a by ORDINAL1:21;
fi1 . a in dom fi2 by ORDINAL4:36;
then A39: fi2 . a in fi2 . (fi1 . a) by A32, A38, ORDINAL2:def 16;
phi . a = fi2 . (fi1 . a) by A35, FUNCT_1:22;
hence contradiction by A32, A34, A35, A39, ORDINAL1:7, ORDINAL4:10; :: thesis: verum
end;
then A40: fi2 . a = a by A34, A35, FUNCT_1:22;
A41: L . a c= Union L by Th24;
let f be Function of VAR ,(L . a); :: thesis: ( Union L,(Union L) ! f |= H iff L . a,f |= H )
thus ( Union L,(Union L) ! f |= H implies L . a,f |= H ) :: thesis: ( L . a,f |= H implies Union L,(Union L) ! f |= H )
proof
assume Union L,(Union L) ! f |= H ; :: thesis: L . a,f |= H
then ( Union L,(Union L) ! f |= the_left_argument_of H & Union L,(Union L) ! f |= the_right_argument_of H & f = (Union L) ! f ) by A29, A41, ZF_LANG1:def 2, ZF_MODEL:15;
then ( L . a,f |= the_left_argument_of H & L . a,f |= the_right_argument_of H ) by A31, A33, A34, A37, A40;
hence L . a,f |= H by A29, ZF_MODEL:15; :: thesis: verum
end;
assume L . a,f |= H ; :: thesis: Union L,(Union L) ! f |= H
then ( L . a,f |= the_left_argument_of H & L . a,f |= the_right_argument_of H ) by A29, ZF_MODEL:15;
then ( Union L,(Union L) ! f |= the_left_argument_of H & Union L,(Union L) ! f |= the_right_argument_of H ) by A31, A33, A34, A37, A40;
hence Union L,(Union L) ! f |= H by A29, ZF_MODEL:15; :: thesis: verum
end;
A42: for H being ZF-formula st H is universal & S1[ the_scope_of H] holds
S1[H]
proof
let H be ZF-formula; :: thesis: ( H is universal & S1[ the_scope_of H] implies S1[H] )
assume H is universal ; :: thesis: ( not S1[ the_scope_of H] or S1[H] )
then A43: H = All (bound_in H),(the_scope_of H) by ZF_LANG:62;
given phi being Ordinal-Sequence of W such that A44: ( phi is increasing & phi is continuous ) and
A45: for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= the_scope_of H iff L . a,f |= the_scope_of H ) ; :: thesis: S1[H]
set x0 = bound_in H;
set H' = the_scope_of H;
A46: now
assume A47: not bound_in H in Free (the_scope_of H) ; :: thesis: S1[H]
thus S1[H] :: thesis: verum
proof
take phi ; :: thesis: ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) )
thus ( phi is increasing & phi is continuous ) by A44; :: thesis: for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H )
let a be Ordinal of W; :: thesis: ( phi . a = a & {} <> a implies for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) )
assume A48: ( phi . a = a & {} <> a ) ; :: thesis: for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H )
let f be Function of VAR ,(L . a); :: thesis: ( Union L,(Union L) ! f |= H iff L . a,f |= H )
thus ( Union L,(Union L) ! f |= H implies L . a,f |= H ) :: thesis: ( L . a,f |= H implies Union L,(Union L) ! f |= H )
proof
assume A49: Union L,(Union L) ! f |= H ; :: thesis: L . a,f |= H
for k being Variable st ((Union L) ! f) . k <> ((Union L) ! f) . k holds
bound_in H = k ;
then Union L,(Union L) ! f |= the_scope_of H by A43, A49, ZF_MODEL:16;
then L . a,f |= the_scope_of H by A45, A48;
hence L . a,f |= H by A43, A47, ZFMODEL1:10; :: thesis: verum
end;
assume A50: L . a,f |= H ; :: thesis: Union L,(Union L) ! f |= H
for k being Variable st f . k <> f . k holds
bound_in H = k ;
then L . a,f |= the_scope_of H by A43, A50, ZF_MODEL:16;
then Union L,(Union L) ! f |= the_scope_of H by A45, A48;
hence Union L,(Union L) ! f |= H by A43, A47, ZFMODEL1:10; :: thesis: verum
end;
end;
defpred S2[ set , set ] means ex f being Function of VAR ,(Union L) st
( $1 = f & ( ex m being Element of Union L st
( m in L . $2 & Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ) or ( $2 = 0-element_of W & ( for m being Element of Union L holds not Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ) ) ) );
A51: for h being Element of Funcs VAR ,(Union L) ex a being Ordinal of W st S2[h,a]
proof
let h be Element of Funcs VAR ,(Union L); :: thesis: ex a being Ordinal of W st S2[h,a]
reconsider f = h as Element of Funcs VAR ,(Union L) ;
reconsider f = f as Function of VAR ,(Union L) by FUNCT_2:121;
now
per cases ( for m being Element of Union L holds not Union L,f / (bound_in H),m |= 'not' (the_scope_of H) or ex m being Element of Union L st Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ) ;
suppose for m being Element of Union L holds not Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ; :: thesis: ex a being Ordinal of W st S2[h,a]
hence ex a being Ordinal of W st S2[h,a] ; :: thesis: verum
end;
suppose A52: ex m being Element of Union L st Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ; :: thesis: ex a being Ordinal of W st S2[h,a]
thus ex a being Ordinal of W st S2[h,a] :: thesis: verum
proof
consider m being Element of Union L such that
A53: Union L,f / (bound_in H),m |= 'not' (the_scope_of H) by A52;
consider X being set such that
A54: ( m in X & X in rng L ) by A3, TARSKI:def 4;
consider x being set such that
A55: ( x in dom L & X = L . x ) by A54, FUNCT_1:def 5;
reconsider x = x as Ordinal by A55;
x in W by A2, A55, ORDINAL1:def 10;
then reconsider b = x as Ordinal of W ;
take b ; :: thesis: S2[h,b]
take f ; :: thesis: ( h = f & ( ex m being Element of Union L st
( m in L . b & Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ) or ( b = 0-element_of W & ( for m being Element of Union L holds not Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ) ) ) )
thus ( h = f & ( ex m being Element of Union L st
( m in L . b & Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ) or ( b = 0-element_of W & ( for m being Element of Union L holds not Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ) ) ) ) by A53, A54, A55; :: thesis: verum
end;
end;
end;
end;
hence ex a being Ordinal of W st S2[h,a] ; :: thesis: verum
end;
consider rho being Function such that
A56: dom rho = Funcs VAR ,(Union L) and
A57: for h being Element of Funcs VAR ,(Union L) ex a being Ordinal of W st
( a = rho . h & S2[h,a] & ( for b being Ordinal of W st S2[h,b] holds
a c= b ) ) from ZF_REFLE:sch 1(A51);
 defpred S3[ Ordinal of W, Ordinal of W] means $2 = sup (rho .: (Funcs VAR ,(L . $1)));
A58: for a, b1, b2 being Ordinal of W st S3[a,b1] & S3[a,b2] holds
b1 = b2 ;
A59: for a being Ordinal of W ex b being Ordinal of W st S3[a,b]
proof
let a be Ordinal of W; :: thesis: ex b being Ordinal of W st S3[a,b]
set X = rho .: (Funcs VAR ,(L . a));
A60: rho .: (Funcs VAR ,(L . a)) c= W
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rho .: (Funcs VAR ,(L . a)) or x in W )
assume x in rho .: (Funcs VAR ,(L . a)) ; :: thesis: x in W
then consider h being set such that
A61: ( h in dom rho & h in Funcs VAR ,(L . a) & x = rho . h ) by FUNCT_1:def 12;
Funcs VAR ,(L . a) c= Funcs VAR ,(Union L) by Th24, FUNCT_5:63;
then reconsider h = h as Element of Funcs VAR ,(Union L) by A61;
ex a being Ordinal of W st
( a = rho . h & ex f being Function of VAR ,(Union L) st
( h = f & ( ex m being Element of Union L st
( m in L . a & Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ) or ( a = 0-element_of W & ( for m being Element of Union L holds not Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ) ) ) ) & ( for b being Ordinal of W st ex f being Function of VAR ,(Union L) st
( h = f & ( ex m being Element of Union L st
( m in L . b & Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ) or ( b = 0-element_of W & ( for m being Element of Union L holds not Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ) ) ) ) holds
a c= b ) ) by A57;
hence x in W by A61; :: thesis: verum
end;
( L . a in W & card VAR = card omega & card (L . a) = card (L . a) ) by Th25, CARD_1:21;
then ( card (Funcs VAR ,(L . a)) = card (Funcs omega ,(L . a)) & Funcs omega ,(L . a) in W ) by A1, CLASSES2:67, FUNCT_5:68;
then ( card (rho .: (Funcs VAR ,(L . a))) c= card (Funcs omega ,(L . a)) & card (Funcs omega ,(L . a)) in card W ) by CARD_2:3, CLASSES2:1;
then ( card (rho .: (Funcs VAR ,(L . a))) in card W & W is Tarski ) by ORDINAL1:22;
then rho .: (Funcs VAR ,(L . a)) in W by A60, CLASSES1:2;
then sup (rho .: (Funcs VAR ,(L . a))) in W by Th28;
then reconsider b = sup (rho .: (Funcs VAR ,(L . a))) as Ordinal of W ;
take b ; :: thesis: S3[a,b]
thus S3[a,b] ; :: thesis: verum
end;
consider si being Ordinal-Sequence of W such that
A62: for a being Ordinal of W holds S3[a,si . a] from ZF_REFLE:sch 2(A58, A59);
 deffunc H1( Ordinal of W, Ordinal of W) -> Element of W = succ ((si . (succ $1)) \/ $2);
deffunc H2( Ordinal of W, Ordinal-Sequence) -> Ordinal of W = union $2,$1;
consider ksi being Ordinal-Sequence of W such that
A63: ksi . (0-element_of W) = si . (0-element_of W) and
A64: for a being Ordinal of W holds ksi . (succ a) = H1(a,ksi . a) and
A65: for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds
ksi . a = H2(a,ksi | a) from ZF_REFLE:sch 3();
 A67: 0-element_of W = {} by ORDINAL4:35;
A68: ksi is increasing
proof
let A be Ordinal; :: according to ORDINAL2:def 16 :: thesis: for b1 being set holds
( not A in b1 or not b1 in dom ksi or ksi . A in ksi . b1 )
let B be Ordinal; :: thesis: ( not A in B or not B in dom ksi or ksi . A in ksi . B )
assume A69: ( A in B & B in dom ksi ) ; :: thesis: ksi . A in ksi . B
then A in dom ksi by ORDINAL1:19;
then reconsider a = A, b = B as Ordinal of W by A69, Th8;
defpred S4[ Ordinal of W] means ( a in $1 implies ksi . a in ksi . $1 );
A70: S4[ 0-element_of W] by ORDINAL4:35;
A71: for c being Ordinal of W st S4[c] holds
S4[ succ c]
proof
let c be Ordinal of W; :: thesis: ( S4[c] implies S4[ succ c] )
assume that
A72: ( a in c implies ksi . a in ksi . c ) and
A73: a in succ c ; :: thesis: ksi . a in ksi . (succ c)
A74: ( a c= c & ksi . (succ c) = succ ((si . (succ c)) \/ (ksi . c)) & (si . (succ c)) \/ (ksi . c) in succ ((si . (succ c)) \/ (ksi . c)) & ksi . c c= (si . (succ c)) \/ (ksi . c) ) by A64, A73, ORDINAL1:34, XBOOLE_1:7;
( ksi . a in ksi . c or ksi . a = ksi . c )
proof
per cases ( a <> c or a = c ) ;
suppose a <> c ; :: thesis: ( ksi . a in ksi . c or ksi . a = ksi . c )
then a c< c by A74, XBOOLE_0:def 8;
hence ( ksi . a in ksi . c or ksi . a = ksi . c ) by A72, ORDINAL1:21; :: thesis: verum
end;
suppose a = c ; :: thesis: ( ksi . a in ksi . c or ksi . a = ksi . c )
hence ( ksi . a in ksi . c or ksi . a = ksi . c ) ; :: thesis: verum
end;
end;
end;
hence ksi . a in ksi . (succ c) by A74, ORDINAL1:19, ORDINAL1:22; :: thesis: verum
end;
A75: for b being Ordinal of W st b <> 0-element_of W & b is limit_ordinal & ( for c being Ordinal of W st c in b holds
S4[c] ) holds
S4[b]
proof
let b be Ordinal of W; :: thesis: ( b <> 0-element_of W & b is limit_ordinal & ( for c being Ordinal of W st c in b holds
S4[c] ) implies S4[b] )
assume that
A76: ( b <> 0-element_of W & b is limit_ordinal ) and
for c being Ordinal of W st c in b holds
S4[c] and
A77: a in b ; :: thesis: ksi . a in ksi . b
A78: ksi . b = union (ksi | b),b by A65, A76
.= Union (ksi | b) by Th17
.= union (rng (ksi | b)) by CARD_3:def 4 ;
( succ a in dom ksi & succ a in b ) by A76, A77, ORDINAL1:41, ORDINAL4:36;
then A79: ksi . (succ a) in rng (ksi | b) by FUNCT_1:73;
ksi . (succ a) = succ ((si . (succ a)) \/ (ksi . a)) by A64;
then ( (si . (succ a)) \/ (ksi . a) in ksi . (succ a) & ksi . a c= (si . (succ a)) \/ (ksi . a) ) by ORDINAL1:10, XBOOLE_1:7;
then ksi . a in ksi . (succ a) by ORDINAL1:22;
hence ksi . a in ksi . b by A78, A79, TARSKI:def 4; :: thesis: verum
end;
for c being Ordinal of W holds S4[c] from ZF_REFLE:sch 4(A70, A71, A75);
 then ksi . a in ksi . b by A69;
hence ksi . A in ksi . B ; :: thesis: verum
end;
defpred S4[ Ordinal] means si . $1 c= ksi . $1;
A80: S4[ 0-element_of W] by A63;
A81: for a being Ordinal of W st S4[a] holds
S4[ succ a]
proof
let a be Ordinal of W; :: thesis: ( S4[a] implies S4[ succ a] )
assume si . a c= ksi . a ; :: thesis: S4[ succ a]
( ksi . (succ a) = succ ((si . (succ a)) \/ (ksi . a)) & (si . (succ a)) \/ (ksi . a) in succ ((si . (succ a)) \/ (ksi . a)) & si . (succ a) c= (si . (succ a)) \/ (ksi . a) ) by A64, ORDINAL1:10, XBOOLE_1:7;
then si . (succ a) in ksi . (succ a) by ORDINAL1:22;
hence si . (succ a) c= ksi . (succ a) by ORDINAL1:def 2; :: thesis: verum
end;
A82: for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds
si . a c= sup (si | a)
proof
let a be Ordinal of W; :: thesis: ( a <> 0-element_of W & a is limit_ordinal implies si . a c= sup (si | a) )
assume A83: ( a <> 0-element_of W & a is limit_ordinal ) ; :: thesis: si . a c= sup (si | a)
let A be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not A in si . a or A in sup (si | a) )
assume A84: A in si . a ; :: thesis: A in sup (si | a)
si . a = sup (rho .: (Funcs VAR ,(L . a))) by A62;
then consider B being Ordinal such that
A85: ( B in rho .: (Funcs VAR ,(L . a)) & A c= B ) by A84, ORDINAL2:29;
consider x being set such that
A86: ( x in dom rho & x in Funcs VAR ,(L . a) & B = rho . x ) by A85, FUNCT_1:def 12;
reconsider h = x as Element of Funcs VAR ,(Union L) by A56, A86;
consider a1 being Ordinal of W such that
A87: ( a1 = rho . h & ex f being Function of VAR ,(Union L) st
( h = f & ( ex m being Element of Union L st
( m in L . a1 & Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ) or ( a1 = 0-element_of W & ( for m being Element of Union L holds not Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ) ) ) ) & ( for b being Ordinal of W st ex f being Function of VAR ,(Union L) st
( h = f & ( ex m being Element of Union L st
( m in L . b & Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ) or ( b = 0-element_of W & ( for m being Element of Union L holds not Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ) ) ) ) holds
a1 c= b ) ) by A57;
consider f being Function of VAR ,(Union L) such that
A88: ( h = f & ( ex m being Element of Union L st
( m in L . a1 & Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ) or ( a1 = 0-element_of W & ( for m being Element of Union L holds not Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ) ) ) ) by A87;
defpred S5[ set , set ] means for a being Ordinal of W st f . $1 in L . a holds
f . $2 in L . a;
A89: now
assume Free ('not' (the_scope_of H)) <> {} ; :: thesis: ex x being Ordinal of W st
( x in a & ( for y being Variable st y in Free ('not' (the_scope_of H)) holds
f . y in L . x ) )
then A90: Free ('not' (the_scope_of H)) <> {} ;
A91: for x, y being set holds
( S5[x,y] or S5[y,x] )
proof
let x, y be set ; :: thesis: ( S5[x,y] or S5[y,x] )
given a being Ordinal of W such that A92: ( f . x in L . a & not f . y in L . a ) ; :: thesis: S5[y,x]
let b be Ordinal of W; :: thesis: ( f . y in L . b implies f . x in L . b )
assume A93: f . y in L . b ; :: thesis: f . x in L . b
( a in b or a = b or b in a ) by ORDINAL1:24;
then ( L . a c= L . b or L . b c= L . a ) by A1;
hence f . x in L . b by A92, A93; :: thesis: verum
end;
A94: for x, y, z being set st S5[x,y] & S5[y,z] holds
S5[x,z] ;
consider z being set such that
A95: ( z in Free ('not' (the_scope_of H)) & ( for y being set st y in Free ('not' (the_scope_of H)) holds
S5[z,y] ) ) from CARD_3:sch 3(A90, A91, A94);
reconsider z = z as Variable by A95;
A96: ex s being Function st
( f = s & dom s = VAR & rng s c= L . a ) by A86, A88, FUNCT_2:def 2;
then f . z in rng f by FUNCT_1:def 5;
then ( f . z in L . a & L . a = Union (L | a) & Union (L | a) = union (rng (L | a)) ) by A1, A67, A83, A96, CARD_3:def 4;
then consider X being set such that
A97: ( f . z in X & X in rng (L | a) ) by TARSKI:def 4;
consider x being set such that
A98: ( x in dom (L | a) & X = (L | a) . x ) by A97, FUNCT_1:def 5;
A99: ( dom (L | a) c= a & (L | a) . x = L . x ) by A98, FUNCT_1:70, RELAT_1:87;
then A100: ( x in a & a in On W ) by A98, Th8;
reconsider x = x as Ordinal by A98;
x in On W by A100, ORDINAL1:19;
then reconsider x = x as Ordinal of W by Th8;
take x = x; :: thesis: ( x in a & ( for y being Variable st y in Free ('not' (the_scope_of H)) holds
f . y in L . x ) )
thus x in a by A98, A99; :: thesis: for y being Variable st y in Free ('not' (the_scope_of H)) holds
f . y in L . x
let y be Variable; :: thesis: ( y in Free ('not' (the_scope_of H)) implies f . y in L . x )
assume y in Free ('not' (the_scope_of H)) ; :: thesis: f . y in L . x
hence f . y in L . x by A95, A97, A98, A99; :: thesis: verum
end;
now
assume A101: Free ('not' (the_scope_of H)) = {} ; :: thesis: ex b being Element of W st
( b in a & ( for x1 being Variable st x1 in Free ('not' (the_scope_of H)) holds
f . x1 in L . b ) )
take b = 0-element_of W; :: thesis: ( b in a & ( for x1 being Variable st x1 in Free ('not' (the_scope_of H)) holds
f . x1 in L . b ) )
thus b in a by A67, A83, ORDINAL3:10; :: thesis: for x1 being Variable st x1 in Free ('not' (the_scope_of H)) holds
f . x1 in L . b
thus for x1 being Variable st x1 in Free ('not' (the_scope_of H)) holds
f . x1 in L . b by A101; :: thesis: verum
end;
then consider c being Ordinal of W such that
A102: ( c in a & ( for x1 being Variable st x1 in Free ('not' (the_scope_of H)) holds
f . x1 in L . c ) ) by A89;
consider e being Element of L . c;
defpred S6[ set ] means $1 in Free ('not' (the_scope_of H));
deffunc H3( set ) -> set = f . $1;
deffunc H4( set ) -> Element of L . c = e;
consider v being Function such that
A103: ( dom v = VAR & ( for x being set st x in VAR holds
( ( S6[x] implies v . x = H3(x) ) & ( not S6[x] implies v . x = H4(x) ) ) ) ) from PARTFUN1:sch 1();
 A104: rng v c= L . c
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng v or x in L . c )
assume x in rng v ; :: thesis: x in L . c
then consider y being set such that
A105: ( y in dom v & x = v . y ) by FUNCT_1:def 5;
reconsider y = y as Variable by A103, A105;
( y in Free ('not' (the_scope_of H)) or not y in Free ('not' (the_scope_of H)) ) ;
then ( ( x = f . y & f . y in L . c ) or x = e ) by A102, A103, A105;
hence x in L . c ; :: thesis: verum
end;
then reconsider v = v as Function of VAR ,(L . c) by A103, FUNCT_2:def 1, RELSET_1:11;
A106: L . c c= Union L by Th24;
then A107: ( v in Funcs VAR ,(L . c) & v = (Union L) ! v & Funcs VAR ,(L . c) c= Funcs VAR ,(Union L) ) by A103, A104, FUNCT_2:def 2, FUNCT_5:63, ZF_LANG1:def 2;
then reconsider v' = v as Element of Funcs VAR ,(Union L) ;
consider a2 being Ordinal of W such that
A108: ( a2 = rho . v' & ex f being Function of VAR ,(Union L) st
( v' = f & ( ex m being Element of Union L st
( m in L . a2 & Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ) or ( a2 = 0-element_of W & ( for m being Element of Union L holds not Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ) ) ) ) & ( for b being Ordinal of W st ex f being Function of VAR ,(Union L) st
( v' = f & ( ex m being Element of Union L st
( m in L . b & Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ) or ( b = 0-element_of W & ( for m being Element of Union L holds not Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ) ) ) ) holds
a2 c= b ) ) by A57;
consider f' being Function of VAR ,(Union L) such that
A109: ( v' = f' & ( ex m being Element of Union L st
( m in L . a2 & Union L,f' / (bound_in H),m |= 'not' (the_scope_of H) ) or ( a2 = 0-element_of W & ( for m being Element of Union L holds not Union L,f' / (bound_in H),m |= 'not' (the_scope_of H) ) ) ) ) by A108;
A110: now
assume A111: for m being Element of Union L holds not Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ; :: thesis: a1 = a2
now
let m be Element of Union L; :: thesis: not Union L,((Union L) ! v) / (bound_in H),m |= 'not' (the_scope_of H)
A112: not Union L,f / (bound_in H),m |= 'not' (the_scope_of H) by A111;
now
let x1 be Variable; :: thesis: ( x1 in Free ('not' (the_scope_of H)) implies (f / (bound_in H),m) . x1 = (((Union L) ! v) / (bound_in H),m) . x1 )
assume x1 in Free ('not' (the_scope_of H)) ; :: thesis: (f / (bound_in H),m) . x1 = (((Union L) ! v) / (bound_in H),m) . x1
then ( f . x1 = ((Union L) ! v) . x1 & (f / (bound_in H),m) . (bound_in H) = m & (((Union L) ! v) / (bound_in H),m) . (bound_in H) = m & ( x1 <> bound_in H implies ( (f / (bound_in H),m) . x1 = f . x1 & (((Union L) ! v) / (bound_in H),m) . x1 = ((Union L) ! v) . x1 ) ) ) by A103, A107, FUNCT_7:34, FUNCT_7:130;
hence (f / (bound_in H),m) . x1 = (((Union L) ! v) / (bound_in H),m) . x1 ; :: thesis: verum
end;
hence not Union L,((Union L) ! v) / (bound_in H),m |= 'not' (the_scope_of H) by A112, ZF_LANG1:84; :: thesis: verum
end;
hence a1 = a2 by A88, A107, A109, A111; :: thesis: verum
end;
now
given m being Element of Union L such that A113: ( m in L . a1 & Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ) ; :: thesis: a1 = a2
now
let x1 be Variable; :: thesis: ( x1 in Free ('not' (the_scope_of H)) implies (f / (bound_in H),m) . x1 = (((Union L) ! v) / (bound_in H),m) . x1 )
assume x1 in Free ('not' (the_scope_of H)) ; :: thesis: (f / (bound_in H),m) . x1 = (((Union L) ! v) / (bound_in H),m) . x1
then ( f . x1 = ((Union L) ! v) . x1 & (f / (bound_in H),m) . (bound_in H) = m & (((Union L) ! v) / (bound_in H),m) . (bound_in H) = m & ( x1 <> bound_in H implies ( (f / (bound_in H),m) . x1 = f . x1 & (((Union L) ! v) / (bound_in H),m) . x1 = ((Union L) ! v) . x1 ) ) ) by A103, A107, FUNCT_7:34, FUNCT_7:130;
hence (f / (bound_in H),m) . x1 = (((Union L) ! v) / (bound_in H),m) . x1 ; :: thesis: verum
end;
then A114: Union L,((Union L) ! v) / (bound_in H),m |= 'not' (the_scope_of H) by A113, ZF_LANG1:84;
then consider m' being Element of Union L such that
A115: ( m' in L . a2 & Union L,f' / (bound_in H),m' |= 'not' (the_scope_of H) ) by A107, A109;
now
let x1 be Variable; :: thesis: ( x1 in Free ('not' (the_scope_of H)) implies (f / (bound_in H),m') . x1 = (f' / (bound_in H),m') . x1 )
assume x1 in Free ('not' (the_scope_of H)) ; :: thesis: (f / (bound_in H),m') . x1 = (f' / (bound_in H),m') . x1
then ( f . x1 = ((Union L) ! v) . x1 & (f / (bound_in H),m') . (bound_in H) = m' & (((Union L) ! v) / (bound_in H),m') . (bound_in H) = m' & ( x1 <> bound_in H implies ( (f / (bound_in H),m') . x1 = f . x1 & (((Union L) ! v) / (bound_in H),m') . x1 = ((Union L) ! v) . x1 ) ) ) by A103, A107, FUNCT_7:34, FUNCT_7:130;
hence (f / (bound_in H),m') . x1 = (f' / (bound_in H),m') . x1 by A106, A109, ZF_LANG1:def 2; :: thesis: verum
end;
then Union L,f / (bound_in H),m' |= 'not' (the_scope_of H) by A115, ZF_LANG1:84;
then ( a1 c= a2 & a2 c= a1 ) by A87, A88, A107, A108, A113, A114, A115;
hence a1 = a2 by XBOOLE_0:def 10; :: thesis: verum
end;
then ( B in rho .: (Funcs VAR ,(L . c)) & si . c = sup (rho .: (Funcs VAR ,(L . c))) & c in dom si & dom (si | a) = (dom si) /\ a ) by A56, A62, A86, A87, A88, A107, A108, A110, FUNCT_1:def 12, ORDINAL4:36, RELAT_1:90;
then A116: ( B in si . c & si . c = (si | a) . c & c in dom (si | a) ) by A102, FUNCT_1:72, ORDINAL2:27, XBOOLE_0:def 4;
then ( si . c in rng (si | a) & sup (si | a) = sup (rng (si | a)) ) by FUNCT_1:def 5;
then si . c in sup (si | a) by ORDINAL2:27;
then B in sup (si | a) by A116, ORDINAL1:19;
hence A in sup (si | a) by A85, ORDINAL1:22; :: thesis: verum
end;
A117: for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal & ( for b being Ordinal of W st b in a holds
S4[b] ) holds
S4[a]
proof
let a be Ordinal of W; :: thesis: ( a <> 0-element_of W & a is limit_ordinal & ( for b being Ordinal of W st b in a holds
S4[b] ) implies S4[a] )
assume that
A118: ( a <> 0-element_of W & a is limit_ordinal ) and
A119: for b being Ordinal of W st b in a holds
si . b c= ksi . b ; :: thesis: S4[a]
thus si . a c= ksi . a :: thesis: verum
proof
let A be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not A in si . a or A in ksi . a )
assume A120: A in si . a ; :: thesis: A in ksi . a
si . a c= sup (si | a) by A82, A118;
then consider B being Ordinal such that
A121: ( B in rng (si | a) & A c= B ) by A120, ORDINAL2:29;
consider x being set such that
A122: ( x in dom (si | a) & B = (si | a) . x ) by A121, FUNCT_1:def 5;
reconsider x = x as Ordinal by A122;
A123: dom (si | a) c= a by RELAT_1:87;
then A124: ( x in a & a in On W ) by A122, Th8;
then x in On W by ORDINAL1:19;
then reconsider x = x as Ordinal of W by Th8;
( si . x = B & si . x c= ksi . x & dom ksi = On W ) by A119, A122, A123, FUNCT_1:70, FUNCT_2:def 1;
then ( A c= ksi . x & ksi . x in ksi . a ) by A68, A121, A124, ORDINAL2:def 16, XBOOLE_1:1;
hence A in ksi . a by ORDINAL1:22; :: thesis: verum
end;
end;
A125: for a being Ordinal of W holds S4[a] from ZF_REFLE:sch 4(A80, A81, A117);
 A126: ksi is continuous
proof
let A be Ordinal; :: according to ORDINAL2:def 17 :: thesis: for b1 being set holds
( not A in dom ksi or A = {} or not A is limit_ordinal or not b1 = ksi . A or b1 is_limes_of ksi | A )
let B be Ordinal; :: thesis: ( not A in dom ksi or A = {} or not A is limit_ordinal or not B = ksi . A or B is_limes_of ksi | A )
assume A127: ( A in dom ksi & A <> {} & A is limit_ordinal & B = ksi . A ) ; :: thesis: B is_limes_of ksi | A
then reconsider a = A as Ordinal of W by Th8;
A c= dom ksi by A127, ORDINAL1:def 2;
then A128: ( dom (ksi | A) = A & ksi | A is increasing ) by A68, ORDINAL4:15, RELAT_1:91;
then A129: ( sup (ksi | A) is_limes_of ksi | A & sup (ksi | A) = sup (rng (ksi | A)) ) by A127, ORDINAL4:8;
A130: B = union (ksi | a),a by A65, A67, A127
.= Union (ksi | a) by Th17
.= union (rng (ksi | a)) by CARD_3:def 4 ;
A131: B c= sup (ksi | A)
proof
let C be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not C in B or C in sup (ksi | A) )
assume C in B ; :: thesis: C in sup (ksi | A)
then consider X being set such that
A132: ( C in X & X in rng (ksi | A) ) by A130, TARSKI:def 4;
consider A1 being Ordinal such that
A133: rng (ksi | A) c= A1 by ORDINAL2:def 8;
reconsider X = X as Ordinal by A132, A133;
X in sup (ksi | A) by A132, ORDINAL2:27;
hence C in sup (ksi | A) by A132, ORDINAL1:19; :: thesis: verum
end;
sup (ksi | A) c= B
proof
let C be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not C in sup (ksi | A) or C in B )
assume C in sup (ksi | A) ; :: thesis: C in B
then consider D being Ordinal such that
A134: ( D in rng (ksi | A) & C c= D ) by ORDINAL2:29;
consider x being set such that
A135: ( x in dom (ksi | A) & D = (ksi | A) . x ) by A134, FUNCT_1:def 5;
reconsider x = x as Ordinal by A135;
( x in succ x & succ x in A ) by A127, A128, A135, ORDINAL1:10, ORDINAL1:41;
then ( D in (ksi | A) . (succ x) & (ksi | A) . (succ x) in rng (ksi | A) ) by A128, A135, FUNCT_1:def 5, ORDINAL2:def 16;
then D in B by A130, TARSKI:def 4;
hence C in B by A134, ORDINAL1:22; :: thesis: verum
end;
hence B is_limes_of ksi | A by A129, A131, XBOOLE_0:def 10; :: thesis: verum
end;
now
assume bound_in H in Free (the_scope_of H) ; :: thesis: S1[H]
thus S1[H] :: thesis: verum
proof
take gamma = phi * ksi; :: thesis: ( gamma is increasing & gamma is continuous & ( for a being Ordinal of W st gamma . a = a & {} <> a holds
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) )
ex f being Ordinal-Sequence st
( f = phi * ksi & f is increasing ) by A44, A68, ORDINAL4:13;
hence ( gamma is increasing & gamma is continuous ) by A44, A68, A126, ORDINAL4:17; :: thesis: for a being Ordinal of W st gamma . a = a & {} <> a holds
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H )
let a be Ordinal of W; :: thesis: ( gamma . a = a & {} <> a implies for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) )
assume A136: ( gamma . a = a & {} <> a ) ; :: thesis: for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H )
( a in dom gamma & ksi . a in dom phi & a in dom ksi ) by ORDINAL4:36;
then ( ksi . a c= phi . (ksi . a) & a c= ksi . a & phi . (ksi . a) = gamma . a ) by A44, A68, FUNCT_1:22, ORDINAL4:10;
then A137: ( ksi . a = a & phi . a = a ) by A136, XBOOLE_0:def 10;
let f be Function of VAR ,(L . a); :: thesis: ( Union L,(Union L) ! f |= H iff L . a,f |= H )
thus ( Union L,(Union L) ! f |= H implies L . a,f |= H ) :: thesis: ( L . a,f |= H implies Union L,(Union L) ! f |= H )
proof
assume A138: Union L,(Union L) ! f |= H ; :: thesis: L . a,f |= H
now
let g be Function of VAR ,(L . a); :: thesis: ( ( for k being Variable st g . k <> f . k holds
bound_in H = k ) implies L . a,g |= the_scope_of H )
assume A139: for k being Variable st g . k <> f . k holds
bound_in H = k ; :: thesis: L . a,g |= the_scope_of H
now
let k be Variable; :: thesis: ( ((Union L) ! g) . k <> ((Union L) ! f) . k implies bound_in H = k )
( (Union L) ! f = f & (Union L) ! g = g ) by Th24, ZF_LANG1:def 2;
hence ( ((Union L) ! g) . k <> ((Union L) ! f) . k implies bound_in H = k ) by A139; :: thesis: verum
end;
then Union L,(Union L) ! g |= the_scope_of H by A43, A138, ZF_MODEL:16;
hence L . a,g |= the_scope_of H by A45, A136, A137; :: thesis: verum
end;
hence L . a,f |= H by A43, ZF_MODEL:16; :: thesis: verum
end;
assume that
A140: L . a,f |= H and
A141: not Union L,(Union L) ! f |= H ; :: thesis: contradiction
consider m being Element of Union L such that
A142: not Union L,((Union L) ! f) / (bound_in H),m |= the_scope_of H by A43, A141, ZF_LANG1:80;
A143: Union L,((Union L) ! f) / (bound_in H),m |= 'not' (the_scope_of H) by A142, ZF_MODEL:14;
A144: ( (Union L) ! f in Funcs VAR ,(Union L) & f in Funcs VAR ,(L . a) ) by FUNCT_2:11;
reconsider h = (Union L) ! f as Element of Funcs VAR ,(Union L) by FUNCT_2:11;
consider a1 being Ordinal of W such that
A145: ( a1 = rho . h & ex f being Function of VAR ,(Union L) st
( h = f & ( ex m being Element of Union L st
( m in L . a1 & Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ) or ( a1 = 0-element_of W & ( for m being Element of Union L holds not Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ) ) ) ) & ( for b being Ordinal of W st ex f being Function of VAR ,(Union L) st
( h = f & ( ex m being Element of Union L st
( m in L . b & Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ) or ( b = 0-element_of W & ( for m being Element of Union L holds not Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ) ) ) ) holds
a1 c= b ) ) by A57;
consider m being Element of Union L such that
A146: ( m in L . a1 & Union L,((Union L) ! f) / (bound_in H),m |= 'not' (the_scope_of H) ) by A143, A145;
A147: (Union L) ! f = f by Th24, ZF_LANG1:def 2;
then ( a1 in rho .: (Funcs VAR ,(L . a)) & si . a = sup (rho .: (Funcs VAR ,(L . a))) ) by A56, A62, A144, A145, FUNCT_1:def 12;
then ( a1 in si . a & si . a c= ksi . a ) by A125, ORDINAL2:27;
then L . a1 c= L . a by A1, A137;
then reconsider m' = m as Element of L . a by A146;
( dom (((Union L) ! f) / (bound_in H),m) = VAR & rng (((Union L) ! f) / (bound_in H),m) c= L . a )
proof
thus dom (((Union L) ! f) / (bound_in H),m) = VAR by FUNCT_2:def 1; :: thesis: rng (((Union L) ! f) / (bound_in H),m) c= L . a
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (((Union L) ! f) / (bound_in H),m) or x in L . a )
assume x in rng (((Union L) ! f) / (bound_in H),m) ; :: thesis: x in L . a
then consider y being set such that
A148: ( y in dom (((Union L) ! f) / (bound_in H),m) & x = (((Union L) ! f) / (bound_in H),m) . y ) by FUNCT_1:def 5;
reconsider y = y as Variable by A148;
( y = bound_in H or y <> bound_in H ) ;
then ( x = m' or x = f . y ) by A147, A148, FUNCT_7:34, FUNCT_7:130;
hence x in L . a ; :: thesis: verum
end;
then reconsider g = ((Union L) ! f) / (bound_in H),m as Function of VAR ,(L . a) by FUNCT_2:def 1, RELSET_1:11;
( g . (bound_in H) = m' & ( for y being Variable st g . y <> f . y holds
bound_in H = y ) ) by A147, FUNCT_7:34, FUNCT_7:130;
then ((Union L) ! f) / (bound_in H),m = f / (bound_in H),m' by FUNCT_7:131;
then ((Union L) ! f) / (bound_in H),m = (Union L) ! (f / (bound_in H),m') by Th24, ZF_LANG1:def 2;
then not Union L,(Union L) ! (f / (bound_in H),m') |= the_scope_of H by A146, ZF_MODEL:14;
then not L . a,f / (bound_in H),m' |= the_scope_of H by A45, A136, A137;
hence contradiction by A43, A140, ZF_LANG1:80; :: thesis: verum
end;
end;
hence S1[H] by A46; :: thesis: verum
end;
thus for H being ZF-formula holds S1[H] from ZF_LANG:sch 1(A4, A22, A28, A42); :: thesis: verum