:: Cardinal Numbers
:: by Grzegorz Bancerek
::
:: Received September 19, 1989
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem Def1 defines cardinal CARD_1:def 1 :
theorem :: CARD_1:1
canceled;
theorem :: CARD_1:2
canceled;
theorem :: CARD_1:3
canceled;
theorem Th4: :: CARD_1:4
theorem :: CARD_1:5
canceled;
theorem :: CARD_1:6
canceled;
theorem :: CARD_1:7
canceled;
theorem Th8: :: CARD_1:8
theorem :: CARD_1:9
canceled;
theorem :: CARD_1:10
canceled;
theorem :: CARD_1:11
canceled;
theorem :: CARD_1:12
canceled;
theorem :: CARD_1:13
theorem :: CARD_1:14
:: deftheorem CARD_1:def 2 :
canceled;
:: deftheorem CARD_1:def 3 :
canceled;
:: deftheorem CARD_1:def 4 :
canceled;
:: deftheorem Def5 defines card CARD_1:def 5 :
theorem :: CARD_1:15
canceled;
theorem :: CARD_1:16
canceled;
theorem :: CARD_1:17
canceled;
theorem :: CARD_1:18
canceled;
theorem :: CARD_1:19
canceled;
theorem :: CARD_1:20
canceled;
theorem Th21: :: CARD_1:21
theorem Th22: :: CARD_1:22
theorem Th23: :: CARD_1:23
theorem Th24: :: CARD_1:24
theorem :: CARD_1:25
theorem Th26: :: CARD_1:26
theorem Th27: :: CARD_1:27
theorem :: CARD_1:28
theorem Th29: :: CARD_1:29
theorem Th30: :: CARD_1:30
:: deftheorem Def6 defines nextcard CARD_1:def 6 :
theorem :: CARD_1:31
canceled;
theorem Th32: :: CARD_1:32
theorem :: CARD_1:33
theorem Th34: :: CARD_1:34
theorem Th35: :: CARD_1:35
theorem :: CARD_1:36
:: deftheorem Def7 defines limit_cardinal CARD_1:def 7 :
:: deftheorem Def8 defines alef CARD_1:def 8 :
deffunc H1( Ordinal) -> set = alef $1;
theorem :: CARD_1:37
canceled;
theorem :: CARD_1:38
canceled;
theorem Th39: :: CARD_1:39
theorem :: CARD_1:40
theorem Th41: :: CARD_1:41
theorem Th42: :: CARD_1:42
theorem :: CARD_1:43
theorem :: CARD_1:44
theorem :: CARD_1:45
theorem Th46: :: CARD_1:46
theorem :: CARD_1:47
theorem Th48: :: CARD_1:48
theorem :: CARD_1:49
theorem :: CARD_1:50
theorem :: CARD_1:51
canceled;
theorem :: CARD_1:52
canceled;
theorem :: CARD_1:53
canceled;
theorem :: CARD_1:54
canceled;
theorem :: CARD_1:55
canceled;
theorem :: CARD_1:56
canceled;
theorem :: CARD_1:57
canceled;
theorem Th58: :: CARD_1:58
theorem Th59: :: CARD_1:59
theorem Th60: :: CARD_1:60
theorem Th61: :: CARD_1:61
theorem Th62: :: CARD_1:62
theorem Th63: :: CARD_1:63
theorem :: CARD_1:64
canceled;
Th64:
for n, m being natural number st n,m are_equipotent holds
n = m
theorem Th65: :: CARD_1:65
theorem :: CARD_1:66
canceled;
theorem :: CARD_1:67
canceled;
theorem Th68: :: CARD_1:68
theorem Th69: :: CARD_1:69
theorem :: CARD_1:70
canceled;
theorem :: CARD_1:71
theorem :: CARD_1:72
theorem Th73: :: CARD_1:73
theorem Th74: :: CARD_1:74
theorem :: CARD_1:75
canceled;
theorem Th76: :: CARD_1:76
theorem :: CARD_1:77
canceled;
theorem :: CARD_1:78
canceled;
theorem :: CARD_1:79
canceled;
theorem :: CARD_1:80
canceled;
theorem :: CARD_1:81
canceled;
theorem :: CARD_1:82
theorem Th83: :: CARD_1:83
theorem :: CARD_1:84
theorem :: CARD_1:85
canceled;
theorem :: CARD_1:86
Th102:
for A being Ordinal
for n being natural number st A,n are_equipotent holds
A = n
Th103:
for A being Ordinal holds
( A is finite iff A in omega )
theorem Th87: :: CARD_1:87
theorem Th88: :: CARD_1:88
theorem Th89: :: CARD_1:89
theorem Th90: :: CARD_1:90
theorem Th91: :: CARD_1:91
theorem Th92: :: CARD_1:92
theorem Th93: :: CARD_1:93
theorem Th94: :: CARD_1:94
theorem Th95: :: CARD_1:95
theorem :: CARD_1:96
10
= {0 ,1,2,3,4,5,6,7,8,9}
theorem :: CARD_1:97
:: deftheorem CARD_1:def 9 :
canceled;
:: deftheorem CARD_1:def 10 :
canceled;
:: deftheorem CARD_1:def 11 :
canceled;
:: deftheorem defines Segm CARD_1:def 12 :
theorem :: CARD_1:98
canceled;
theorem :: CARD_1:99
canceled;
theorem :: CARD_1:100
canceled;
theorem :: CARD_1:101
canceled;
theorem :: CARD_1:102
theorem :: CARD_1:103