:: ZFREFLE1 semantic presentation

definition

let c₁ be non empty set ;
let c₂ be Subset of WFF ;
pred c₁ |= c₂ means :Def1: :: ZFREFLE1:def 1
for b₁ being ZF-formula st b₁ in a₂ holds
a₁ |= b₁;

end;

:: deftheorem Def1 defines |= ZFREFLE1:def 1 :

definition

let c₁, c₂ be non empty set ;
pred c₁ <==> c₂ means :: ZFREFLE1:def 2
for b₁ being ZF-formula st Free b₁ = {} holds
( a₁ |= b₁ iff a₂ |= b₁ );
reflexivity ;
symmetry ;
pred c₁ is_elementary_subsystem_of c₂ means :: ZFREFLE1:def 3
( a₁ c= a₂ & ( for b₁ being ZF-formula
for b₂ being Function of VAR ,a₁ holds
( a₁,b₂ |= b₁ iff a₂,a₂ ! b₂ |= b₁ ) ) );
reflexivity by ZF_LANG1:def 2;

end;

:: deftheorem Def2 defines <==> ZFREFLE1:def 2 :

:: deftheorem Def3 defines is_elementary_subsystem_of ZFREFLE1:def 3 :

defpred S₁[ set ] means ( a₁ = the_axiom_of_extensionality or a₁ = the_axiom_of_pairs or a₁ = the_axiom_of_unions or a₁ = the_axiom_of_infinity or a₁ = the_axiom_of_power_sets or ex b₁ being ZF-formula st
( {(x. 0),(x. 1),(x. 2)} misses Free b₁ & a₁ = the_axiom_of_substitution_for b₁ ) );

definition

func ZF-axioms -> set means :Def4: :: ZFREFLE1:def 4
for b₁ being set holds
( b₁ in a₁ iff ( b₁ in WFF & ( b₁ = the_axiom_of_extensionality or b₁ = the_axiom_of_pairs or b₁ = the_axiom_of_unions or b₁ = the_axiom_of_infinity or b₁ = the_axiom_of_power_sets or ex b₂ being ZF-formula st
( {(x. 0),(x. 1),(x. 2)} misses Free b₂ & b₁ = the_axiom_of_substitution_for b₂ ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines ZF-axioms ZFREFLE1:def 4 :

definition

redefine func ZF-axioms as ZF-axioms -> Subset of WFF ;
coherence

proof end;

end;

theorem Th1: :: ZFREFLE1:1

for b₁ being non empty set holds b₁ |= {} WFF

proof end;

theorem Th2: :: ZFREFLE1:2

for b₁ being non empty set
for b₂, b₃ being Subset of WFF st b₂ c= b₃ & b₁ |= b₃ holds
b₁ |= b₂

proof end;

theorem Th3: :: ZFREFLE1:3

for b₁ being non empty set
for b₂, b₃ being Subset of WFF st b₁ |= b₂ & b₁ |= b₃ holds
b₁ |= b₂ \/ b₃

proof end;

theorem Th4: :: ZFREFLE1:4

for b₁ being non empty set st b₁ is_a_model_of_ZF holds
b₁ |= ZF-axioms

proof end;

theorem Th5: :: ZFREFLE1:5

for b₁ being non empty set st b₁ |= ZF-axioms & b₁ is epsilon-transitive holds
b₁ is_a_model_of_ZF

proof end;

theorem Th6: :: ZFREFLE1:6

for b₁ being ZF-formula ex b₂ being ZF-formula st
( Free b₂ = {} & ( for b₃ being non empty set holds
( b₃ |= b₂ iff b₃ |= b₁ ) ) )

proof end;

theorem Th7: :: ZFREFLE1:7

for b₁, b₂ being non empty set holds
( b₁ <==> b₂ iff for b₃ being ZF-formula holds
( b₁ |= b₃ iff b₂ |= b₃ ) )

proof end;

theorem Th8: :: ZFREFLE1:8

for b₁, b₂ being non empty set holds
( b₁ <==> b₂ iff for b₃ being Subset of WFF holds
( b₁ |= b₃ iff b₂ |= b₃ ) )

proof end;

theorem Th9: :: ZFREFLE1:9

for b₁, b₂ being non empty set st b₁ is_elementary_subsystem_of b₂ holds
b₁ <==> b₂

proof end;

theorem Th10: :: ZFREFLE1:10

for b₁, b₂ being non empty set st b₁ is_a_model_of_ZF & b₁ <==> b₂ & b₂ is epsilon-transitive holds
b₂ is_a_model_of_ZF

proof end;

scheme :: ZFREFLE1:sch 1
s1{ F₁() -> set , P₁[ set , set ] } :

ex b₁ being Function st
( dom b₁ = F₁() & ( for b₂ being set st b₂ in F₁() holds
P₁[b₂,b₁ . b₂] ) )

provided

E9: for b₁ being set st b₁ in F₁() holds
ex b₂ being set st P₁[b₁,b₂]

proof end;

theorem Th11: :: ZFREFLE1:11

canceled;

theorem Th12: :: ZFREFLE1:12

for b₁ being Function
for b₂ being Universe st dom b₁ in b₂ & rng b₁ c= b₂ holds
rng b₁ in b₂

proof end;

theorem Th13: :: ZFREFLE1:13

for b₁, b₂ being set st ( b₁,b₂ are_equipotent or Card b₁ = Card b₂ ) holds
( bool b₁, bool b₂ are_equipotent & Card (bool b₁) = Card (bool b₂) )

proof end;

theorem Th14: :: ZFREFLE1:14

for b₁ being Universe
for b₂ being non empty set
for b₃ being Function of b₂, Funcs (On b₁),(On b₁) st Card b₂ <` Card b₁ holds
ex b₄ being Ordinal-Sequence of b₁ st
( b₄ is increasing & b₄ is continuous & b₄ . (0-element_of b₁) = 0-element_of b₁ & ( for b₅ being Ordinal of b₁ holds b₄ . (succ b₅) = sup ({(b₄ . b₅)} \/ ((uncurry b₃) .: [:b₂,{(succ b₅)}:])) ) & ( for b₅ being Ordinal of b₁ st b₅ <> 0-element_of b₁ & b₅ is_limit_ordinal holds
b₄ . b₅ = sup (b₄ | b₅) ) )

proof end;

theorem Th15: :: ZFREFLE1:15

for b₁ being Ordinal
for b₂ being Ordinal-Sequence st b₂ is increasing holds
b₁ +^ b₂ is increasing

proof end;

theorem Th16: :: ZFREFLE1:16

for b₁, b₂ being Ordinal
for b₃ being Ordinal-Sequence holds (b₁ +^ b₃) | b₂ = b₁ +^ (b₃ | b₂)

proof end;

theorem Th17: :: ZFREFLE1:17

for b₁ being Ordinal
for b₂ being Ordinal-Sequence st b₂ is increasing & b₂ is continuous holds
b₁ +^ b₂ is continuous

proof end;

definition

let c₁, c₂ be Ordinal;
pred c₁ is_cofinal_with c₂ means :: ZFREFLE1:def 5
ex b₁ being Ordinal-Sequence st
( dom b₁ = a₂ & rng b₁ c= a₁ & b₁ is increasing & a₁ = sup b₁ );
reflexivity

proof end;

end;

:: deftheorem Def5 defines is_cofinal_with ZFREFLE1:def 5 :

theorem Th18: :: ZFREFLE1:18

canceled;

theorem Th19: :: ZFREFLE1:19

for b₁ being set
for b₂ being Ordinal-Sequence st b₁ in rng b₂ holds
b₁ is Ordinal

proof end;

theorem Th20: :: ZFREFLE1:20

for b₁ being Ordinal-Sequence holds rng b₁ c= sup b₁

proof end;

theorem Th21: :: ZFREFLE1:21

for b₁, b₂, b₃ being Ordinal st b₁ is_cofinal_with b₂ & b₂ is_cofinal_with b₃ holds
b₁ is_cofinal_with b₃

proof end;

theorem Th22: :: ZFREFLE1:22

for b₁, b₂ being Ordinal st b₁ is_cofinal_with b₂ holds
b₂ c= b₁

proof end;

theorem Th23: :: ZFREFLE1:23

for b₁, b₂ being Ordinal st b₁ is_cofinal_with b₂ & b₂ is_cofinal_with b₁ holds
b₁ = b₂

proof end;

theorem Th24: :: ZFREFLE1:24

for b₁ being Ordinal
for b₂ being Ordinal-Sequence st dom b₂ <> {} & dom b₂ is_limit_ordinal & b₂ is increasing & b₁ is_limes_of b₂ holds
b₁ is_cofinal_with dom b₂

proof end;

theorem Th25: :: ZFREFLE1:25

for b₁ being Ordinal holds succ b₁ is_cofinal_with one

proof end;

theorem Th26: :: ZFREFLE1:26

for b₁, b₂ being Ordinal st b₁ is_cofinal_with succ b₂ holds
ex b₃ being Ordinal st b₁ = succ b₃

proof end;

theorem Th27: :: ZFREFLE1:27

for b₁, b₂ being Ordinal st b₁ is_cofinal_with b₂ holds
( b₁ is_limit_ordinal iff b₂ is_limit_ordinal )

proof end;

theorem Th28: :: ZFREFLE1:28

for b₁ being Ordinal st b₁ is_cofinal_with {} holds
b₁ = {}

proof end;

theorem Th29: :: ZFREFLE1:29

for b₁ being Universe
for b₂ being Ordinal of b₁ holds not On b₁ is_cofinal_with b₂

proof end;

theorem Th30: :: ZFREFLE1:30

for b₁ being Universe
for b₂ being Ordinal of b₁
for b₃ being Ordinal-Sequence of b₁ st omega in b₁ & b₃ is increasing & b₃ is continuous holds
ex b₄ being Ordinal of b₁ st
( b₂ in b₄ & b₃ . b₄ = b₄ )

proof end;

theorem Th31: :: ZFREFLE1:31

proof end;

theorem Th32: :: ZFREFLE1:32

for b₁ being Universe
for b₂ being DOMAIN-Sequence of b₁ st omega in b₁ & ( for b₃, b₄ being Ordinal of b₁ st b₃ in b₄ holds
b₂ . b₃ c= b₂ . b₄ ) & ( for b₃ being Ordinal of b₁ st b₃ <> {} & b₃ is_limit_ordinal holds
b₂ . b₃ = Union (b₂ | b₃) ) holds
ex b₃ being Ordinal-Sequence of b₁ st
( b₃ is increasing & b₃ is continuous & ( for b₄ being Ordinal of b₁ st b₃ . b₄ = b₄ & {} <> b₄ holds
b₂ . b₄ is_elementary_subsystem_of Union b₂ ) )

proof end;

theorem Th33: :: ZFREFLE1:33

for b₁ being Universe
for b₂ being Ordinal of b₁ holds Rank b₂ in b₁

proof end;

theorem Th34: :: ZFREFLE1:34

for b₁ being Universe
for b₂ being Ordinal of b₁ st b₂ <> {} holds
Rank b₂ is non empty Element of b₁

proof end;

theorem Th35: :: ZFREFLE1:35

for b₁ being Universe st omega in b₁ holds
ex b₂ being Ordinal-Sequence of b₁ st
( b₂ is increasing & b₂ is continuous & ( for b₃ being Ordinal of b₁
for b₄ being non empty set st b₂ . b₃ = b₃ & {} <> b₃ & b₄ = Rank b₃ holds
b₄ is_elementary_subsystem_of b₁ ) )

proof end;

theorem Th36: :: ZFREFLE1:36

for b₁ being Universe
for b₂ being Ordinal of b₁ st omega in b₁ holds
ex b₃ being Ordinal of b₁ex b₄ being non empty set st
( b₂ in b₃ & b₄ = Rank b₃ & b₄ is_elementary_subsystem_of b₁ )

proof end;

theorem Th37: :: ZFREFLE1:37

for b₁ being Universe st omega in b₁ holds
ex b₂ being Ordinal of b₁ex b₃ being non empty set st
( b₂ is_cofinal_with omega & b₃ = Rank b₂ & b₃ is_elementary_subsystem_of b₁ )

proof end;

theorem Th38: :: ZFREFLE1:38

proof end;

theorem Th39: :: ZFREFLE1:39

proof end;

theorem Th40: :: ZFREFLE1:40

for b₁ being Universe
for b₂ being Ordinal of b₁ st omega in b₁ holds
ex b₃ being Ordinal of b₁ex b₄ being non empty set st
( b₂ in b₃ & b₄ = Rank b₃ & b₄ <==> b₁ )

proof end;

theorem Th41: :: ZFREFLE1:41

for b₁ being Universe st omega in b₁ holds
ex b₂ being Ordinal of b₁ex b₃ being non empty set st
( b₂ is_cofinal_with omega & b₃ = Rank b₂ & b₃ <==> b₁ )

proof end;

theorem Th42: :: ZFREFLE1:42

for b₁ being Universe st omega in b₁ holds
ex b₂ being Ordinal of b₁ex b₃ being non empty set st
( b₂ is_cofinal_with omega & b₃ = Rank b₂ & b₃ is_a_model_of_ZF )

proof end;

theorem Th43: :: ZFREFLE1:43

for b₁ being set
for b₂ being Universe st omega in b₂ & b₁ in b₂ holds
ex b₃ being non empty set st
( b₁ in b₃ & b₃ in b₂ & b₃ is_a_model_of_ZF )

proof end;