:: The Reflection Theorem
:: by Grzegorz Bancerek
::
:: Received August 10, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

theorem Th1: :: ZF_REFLE:1
for W being Universe holds W |= the_axiom_of_pairs
proofend;

theorem Th2: :: ZF_REFLE:2
for W being Universe holds W |= the_axiom_of_unions
proofend;

theorem Th3: :: ZF_REFLE:3
for W being Universe st omega in W holds
W |= the_axiom_of_infinity
proofend;

theorem Th4: :: ZF_REFLE:4
for W being Universe holds W |= the_axiom_of_power_sets
proofend;

theorem Th5: :: ZF_REFLE:5
for W being Universe
for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
W |= the_axiom_of_substitution_for H
proofend;

theorem Th6: :: ZF_REFLE:6
for W being Universe st omega in W holds
W is being_a_model_of_ZF
proofend;

scheme :: ZF_REFLE:sch 1
ALFA9Universe{ F1() ->  Universe, F2() ->  non empty set , P1[ set , set ] } :
 ex F being Function st
( dom F = F2() & ( for d being Element of F2() ex a being Ordinal of F1() st
( a = F . d & P1[d,a] & ( for b being Ordinal of F1() st P1[d,b] holds
a c= b ) ) ) )
provided
A1: for d being Element of F2() ex a being Ordinal of F1() st P1[d,a]
proofend;

theorem :: ZF_REFLE:7
for W being Universe
for x being set holds
( x is Ordinal of W iff x in On W ) by ORDINAL1:def_9;

scheme :: ZF_REFLE:sch 2
OrdSeqOfUnivEx{ F1() ->  Universe, P1[ set , set ] } :
 ex phi being Ordinal-Sequence of F1() st
for a being Ordinal of F1() holds P1[a,phi . a]
provided
A1: for a being Ordinal of F1() ex b being Ordinal of F1() st P1[a,b]
proofend;

scheme :: ZF_REFLE:sch 3
UOSExist{ F1() ->  Universe, F2() ->  Ordinal of F1(), F3( Ordinal, Ordinal) ->  Ordinal of F1(), F4( Ordinal, T-Sequence) ->  Ordinal of F1() } :
 ex phi being Ordinal-Sequence of F1() st
( phi . (0-element_of F1()) = F2() &amp; ( for a being Ordinal of F1() holds phi . (succ a) = F3(a,(phi . a)) ) &amp; ( for a being Ordinal of F1() st a <> 0-element_of F1() &amp; a is limit_ordinal holds
phi . a = F4(a,(phi | a)) ) )
proofend;

scheme :: ZF_REFLE:sch 4
UniverseInd{ F1() ->  Universe, P1[ Ordinal] } :
 for a being Ordinal of F1() holds P1[a]
provided
A1: P1[ 0-element_of F1()] and
A2: for a being Ordinal of F1() st P1[a] holds
P1[ succ a] and
A3: for a being Ordinal of F1() st a <> 0-element_of F1() &amp; a is limit_ordinal &amp; ( for b being Ordinal of F1() st b in a holds
P1[b] ) holds
P1[a]
proofend;

definition
let f be Function;
let W be Universe;
let a be Ordinal of W;
func union (f,a) ->  set  equals :: ZF_REFLE:def 1
 Union (W |` (f | (Rank a)));
correctness
coherence
Union (W |` (f | (Rank a))) is set ;
;
end;

:: deftheorem  defines union ZF_REFLE:def_1_:_
 for f being Function
for W being Universe
for a being Ordinal of W holds union (f,a) = Union (W |` (f | (Rank a)));

theorem Th8: :: ZF_REFLE:8
for L being T-Sequence
for A being Ordinal holds L | (Rank A) is T-Sequence
proofend;

theorem Th9: :: ZF_REFLE:9
for L being Ordinal-Sequence
for A being Ordinal holds L | (Rank A) is Ordinal-Sequence
proofend;

theorem :: ZF_REFLE:10
for psi being Ordinal-Sequence holds Union psi is Ordinal ;

theorem Th11: :: ZF_REFLE:11
for X being set
for psi being Ordinal-Sequence holds Union (X |` psi) is Ordinal
proofend;

theorem Th12: :: ZF_REFLE:12
for A being Ordinal holds On (Rank A) = A
proofend;

theorem Th13: :: ZF_REFLE:13
for A being Ordinal
for psi being Ordinal-Sequence holds psi | (Rank A) = psi | A
proofend;

definition
let phi be Ordinal-Sequence;
let W be Universe;
let a be Ordinal of W;
:: original:union
redefine func union (phi,a) ->  Ordinal of W;
coherence
 union (phi,a) is Ordinal of W
proofend;
end;

theorem Th14: :: ZF_REFLE:14
for W being Universe
for a being Ordinal of W
for phi being Ordinal-Sequence of W holds
( union (phi,a) = Union (phi | a) &amp; union ((phi | a),a) = Union (phi | a) )
proofend;

definition
let W be Universe;
let a, b be Ordinal of W;
:: original:\/
redefine funca \/ b ->  Ordinal of W;
coherence
 a \/ b is Ordinal of W
proofend;
end;

registration
let W be Universe;
cluster non empty for Element of W;
existence
 not for b1 being Element of W holds b1 is empty
proofend;
end;

definition
let W be Universe;
mode Subclass of W is non empty Subset of W;
end;

definition
let W be Universe;
let IT be T-Sequence of W;
attrIT is DOMAIN-yielding  means :Def2: :: ZF_REFLE:def 2
 dom IT = On W;
end;

:: deftheorem Def2 defines DOMAIN-yielding ZF_REFLE:def_2_:_
 for W being Universe
for IT being T-Sequence of W holds
( IT is DOMAIN-yielding iff dom IT = On W );

registration
let W be Universe;
cluster Relation-like non-empty W -valued T-Sequence-like Function-like DOMAIN-yielding for set ;
existence
 ex b1 being T-Sequence of W st
( b1 is DOMAIN-yielding &amp; b1 is non-empty )
proofend;
end;

definition
let W be Universe;
mode DOMAIN-Sequence of W is non-empty DOMAIN-yielding T-Sequence of W;
end;

definition
let W be Universe;
let L be DOMAIN-Sequence of W;
:: original:Union
redefine func Union L ->  Subclass of W;
coherence
 Union L is Subclass of W
proofend;
let a be Ordinal of W;
:: original:.
redefine funcL . a ->  non empty Element of W;
coherence
 L . a is non empty Element of W
proofend;
end;

theorem Th15: :: ZF_REFLE:15
for W being Universe
for a being Ordinal of W
for L being DOMAIN-Sequence of W holds a in dom L
proofend;

theorem Th16: :: ZF_REFLE:16
for W being Universe
for a being Ordinal of W
for L being DOMAIN-Sequence of W holds L . a c= Union L
proofend;

theorem Th17: :: ZF_REFLE:17
NAT , VAR are_equipotent
proofend;

theorem :: ZF_REFLE:18
for X being set holds sup X c= succ (union (On X)) by ORDINAL3:72;

theorem Th19: :: ZF_REFLE:19
for W being Universe
for X being set st X in W holds
sup X in W
proofend;

:: [WP: ] Reflection_Theorem
theorem :: ZF_REFLE:20
for W being Universe
for L being DOMAIN-Sequence of W st omega in W &amp; ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) &amp; ( for a being Ordinal of W st a <> {} &amp; 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 &amp; phi is continuous &amp; ( for a being Ordinal of W st phi . a = a &amp; {} <> a holds
for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) )
proofend;

begin

theorem :: ZF_REFLE:21
for M being non countable Aleph st M is strongly_inaccessible holds
Rank M is being_a_model_of_ZF
proofend;