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

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{ F₁() -> Universe, F₂() -> non empty set , P₁[ set , set ] } :

ex F being Function st
( dom F = F₂() & ( for d being Element of F₂() ex a being Ordinal of F₁() st
( a = F . d & P₁[d,a] & ( for b being Ordinal of F₁() st P₁[d,b] holds
a c= b ) ) ) )

provided

A1: for d being Element of F₂() ex a being Ordinal of F₁() st P₁[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{ F₁() -> Universe, P₁[ object , object ] } :

ex phi being Ordinal-Sequence of F₁() st
for a being Ordinal of F₁() holds P₁[a,phi . a]

provided

A1: for a being Ordinal of F₁() ex b being Ordinal of F₁() st P₁[a,b]

proof end;

scheme :: ZF_REFLE:sch 3
UOSExist{ F₁() -> Universe, F₂() -> Ordinal of F₁(), F₃( Ordinal, Ordinal) -> Ordinal of F₁(), F₄( Ordinal, Sequence) -> Ordinal of F₁() } :

ex phi being Ordinal-Sequence of F₁() st
( phi . (0-element_of F₁()) = F₂() & ( for a being Ordinal of F₁() holds phi . (succ a) = F₃(a,(phi . a)) ) & ( for a being Ordinal of F₁() st a <> 0-element_of F₁() & a is limit_ordinal holds
phi . a = F₄(a,(phi | a)) ) )

proof end;

scheme :: ZF_REFLE:sch 4
UniverseInd{ F₁() -> Universe, P₁[ Ordinal] } :

for a being Ordinal of F₁() holds P₁[a]

provided

A1: P₁[ 0-element_of F₁()] and
A2: for a being Ordinal of F₁() st P₁[a] holds
P₁[ succ a] and
A3: for a being Ordinal of F₁() st a <> 0-element_of F₁() & a is limit_ordinal & ( for b being Ordinal of F₁() st b in a holds
P₁[b] ) holds
P₁[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 Sequence
for A being Ordinal holds L | (Rank A) is 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 epsilon-transitive epsilon-connected set

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 b₁ being Element of W holds b₁ 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 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 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 Sequence-like Function-like DOMAIN-yielding for set ;

existence
ex b₁ being Sequence of W st
( b₁ is DOMAIN-yielding & b₁ is non-empty )

proof end;

end;

definition

let W be Universe;
mode DOMAIN-Sequence of W is non-empty DOMAIN-yielding 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;

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

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;