:: The Ordinal Numbers. Transfinite Induction and Defining byTransfinite Induction
:: by Grzegorz Bancerek
::
:: Received March 20, 1989
:: Copyright (c) 1990 Association of Mizar Users
theorem :: ORDINAL1:1
canceled;
theorem :: ORDINAL1:2
canceled;
theorem Th3: :: ORDINAL1:3
for
X,
Y,
Z being
set holds
( not
X in Y or not
Y in Z or not
Z in X )
theorem :: ORDINAL1:4
for
X1,
X2,
X3,
X4 being
set holds
( not
X1 in X2 or not
X2 in X3 or not
X3 in X4 or not
X4 in X1 )
theorem :: ORDINAL1:5
for
X1,
X2,
X3,
X4,
X5 being
set holds
( not
X1 in X2 or not
X2 in X3 or not
X3 in X4 or not
X4 in X5 or not
X5 in X1 )
theorem :: ORDINAL1:6
for
X1,
X2,
X3,
X4,
X5,
X6 being
set holds
( not
X1 in X2 or not
X2 in X3 or not
X3 in X4 or not
X4 in X5 or not
X5 in X6 or not
X6 in X1 )
theorem Th7: :: ORDINAL1:7
for
Y,
X being
set st
Y in X holds
not
X c= Y
:: deftheorem defines succ ORDINAL1:def 1 :
theorem :: ORDINAL1:8
canceled;
theorem :: ORDINAL1:9
canceled;
theorem Th10: :: ORDINAL1:10
theorem :: ORDINAL1:11
canceled;
theorem :: ORDINAL1:12
theorem Th13: :: ORDINAL1:13
for
x,
X being
set holds
(
x in succ X iff (
x in X or
x = X ) )
theorem Th14: :: ORDINAL1:14
:: deftheorem Def2 defines epsilon-transitive ORDINAL1:def 2 :
:: deftheorem Def3 defines epsilon-connected ORDINAL1:def 3 :
Lm1:
( {} is epsilon-transitive & {} is epsilon-connected )
:: deftheorem Def4 defines ordinal ORDINAL1:def 4 :
theorem :: ORDINAL1:15
canceled;
theorem :: ORDINAL1:16
canceled;
theorem :: ORDINAL1:17
canceled;
theorem :: ORDINAL1:18
canceled;
theorem Th19: :: ORDINAL1:19
theorem :: ORDINAL1:20
canceled;
theorem Th21: :: ORDINAL1:21
theorem :: ORDINAL1:22
theorem Th23: :: ORDINAL1:23
theorem Th24: :: ORDINAL1:24
:: deftheorem defines c= ORDINAL1:def 5 :
theorem :: ORDINAL1:25
theorem Th26: :: ORDINAL1:26
theorem :: ORDINAL1:27
canceled;
theorem :: ORDINAL1:28
canceled;
theorem Th29: :: ORDINAL1:29
theorem Th30: :: ORDINAL1:30
theorem Th31: :: ORDINAL1:31
theorem Th32: :: ORDINAL1:32
theorem Th33: :: ORDINAL1:33
theorem Th34: :: ORDINAL1:34
theorem Th35: :: ORDINAL1:35
theorem Th36: :: ORDINAL1:36
theorem Th37: :: ORDINAL1:37
for
X being
set holds
not for
x being
set holds
(
x in X iff
x is
Ordinal )
theorem Th38: :: ORDINAL1:38
theorem :: ORDINAL1:39
:: deftheorem Def6 defines limit_ordinal ORDINAL1:def 6 :
theorem :: ORDINAL1:40
canceled;
theorem Th41: :: ORDINAL1:41
theorem :: ORDINAL1:42
:: deftheorem Def7 defines T-Sequence-like ORDINAL1:def 7 :
:: deftheorem Def8 defines T-Sequence ORDINAL1:def 8 :
theorem :: ORDINAL1:43
canceled;
theorem :: ORDINAL1:44
canceled;
theorem :: ORDINAL1:45
theorem :: ORDINAL1:46
theorem Th47: :: ORDINAL1:47
theorem :: ORDINAL1:48
:: deftheorem Def9 defines c=-linear ORDINAL1:def 9 :
theorem :: ORDINAL1:49
theorem :: ORDINAL1:50
:: deftheorem Def10 defines On ORDINAL1:def 10 :
for
X,
b2 being
set holds
(
b2 = On X iff for
x being
set holds
(
x in b2 iff (
x in X &
x is
Ordinal ) ) );
:: deftheorem defines Lim ORDINAL1:def 11 :
theorem Th51: :: ORDINAL1:51
:: deftheorem Def12 defines omega ORDINAL1:def 12 :
:: deftheorem Def13 defines natural ORDINAL1:def 13 :
theorem :: ORDINAL1:52