:: 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
proof end;

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

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

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

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
proof end;

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

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]
proof end;

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]
proof end;

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() & ( for a being Ordinal of F1() holds phi . (succ a) = F3(a,(phi . a)) ) & ( for a being Ordinal of F1() st a <> 0-element_of F1() & a is limit_ordinal holds
phi . a = F4(a,(phi | a)) ) )
proof end;

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() & a is limit_ordinal & ( for b being Ordinal of F1() st b in a holds
P1[b] ) holds
P1[a]
proof end;

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
proof end;

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

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
proof end;

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

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

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
proof end;
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) & union ((phi | a),a) = Union (phi | a) )
proof end;

definition
let W be Universe;
let a, b be Ordinal of W;
:: original: \/
redefine func a \/ b -> Ordinal of W;
coherence
a \/ b is Ordinal of W
proof end;
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
proof end;
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;
attr IT 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 & b1 is non-empty )
proof end;
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
proof end;
let a be Ordinal of W;
:: original: .
redefine func L . a -> non empty Element of W;
coherence
L . a is non empty Element of W
proof end;
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
proof end;

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
proof end;

theorem Th17: :: ZF_REFLE:17
NAT , VAR are_equipotent
proof end;

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
proof end;

:: WP: Reflection Theorem
theorem :: ZF_REFLE:20
for W being Universe
for L being DOMAIN-Sequence of W 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 ) ) )
proof end;

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
proof end;