:: Consequences of the Reflection Theorem
:: by Grzegorz Bancerek
::
:: Received August 13, 1990
:: Copyright (c) 1990 Association of Mizar Users
Lm1:
{} in omega
by ORDINAL1:def 12;
Lm2:
omega is limit_ordinal
by ORDINAL1:def 12;
:: deftheorem Def1 defines |= ZFREFLE1:def 1 :
:: deftheorem defines <==> ZFREFLE1:def 2 :
:: deftheorem defines is_elementary_subsystem_of ZFREFLE1:def 3 :
defpred S1[ set ] means ( $1 = the_axiom_of_extensionality or $1 = the_axiom_of_pairs or $1 = the_axiom_of_unions or $1 = the_axiom_of_infinity or $1 = the_axiom_of_power_sets or ex H being ZF-formula st
( {(x. 0 ),(x. 1),(x. 2)} misses Free H & $1 = the_axiom_of_substitution_for H ) );
:: deftheorem Def4 defines ZF-axioms ZFREFLE1:def 4 :
theorem :: ZFREFLE1:1
theorem :: ZFREFLE1:2
theorem :: ZFREFLE1:3
theorem Th4: :: ZFREFLE1:4
theorem Th5: :: ZFREFLE1:5
theorem Th6: :: ZFREFLE1:6
theorem :: ZFREFLE1:7
theorem Th8: :: ZFREFLE1:8
theorem Th9: :: ZFREFLE1:9
theorem Th10: :: ZFREFLE1:10
theorem :: ZFREFLE1:11
canceled;
theorem Th12: :: ZFREFLE1:12
theorem :: ZFREFLE1:13
theorem Th14: :: ZFREFLE1:14
theorem Th15: :: ZFREFLE1:15
theorem Th16: :: ZFREFLE1:16
theorem Th17: :: ZFREFLE1:17
theorem :: ZFREFLE1:18
canceled;
theorem :: ZFREFLE1:19
theorem :: ZFREFLE1:20
theorem :: ZFREFLE1:21
theorem Th22: :: ZFREFLE1:22
theorem :: ZFREFLE1:23
theorem :: ZFREFLE1:24
theorem :: ZFREFLE1:25
theorem :: ZFREFLE1:26
theorem :: ZFREFLE1:27
theorem :: ZFREFLE1:28
theorem :: ZFREFLE1:29
theorem Th30: :: ZFREFLE1:30
theorem Th31: :: ZFREFLE1:31
theorem Th32: :: ZFREFLE1:32
theorem Th33: :: ZFREFLE1:33
theorem Th34: :: ZFREFLE1:34
theorem Th35: :: ZFREFLE1:35
theorem Th36: :: ZFREFLE1:36
theorem Th37: :: ZFREFLE1:37
theorem :: ZFREFLE1:38
theorem :: ZFREFLE1:39
theorem Th40: :: ZFREFLE1:40
theorem Th41: :: ZFREFLE1:41
theorem :: ZFREFLE1:42
theorem :: ZFREFLE1:43