:: On Powers of Cardinals
:: by Grzegorz Bancerek
::
:: Received August 24, 1992
:: Copyright (c) 1992 Association of Mizar Users
Lm1:
( 0 = card 0 & 1 = card 1 & 2 = card 2 )
by CARD_1:def 5;
theorem :: CARD_5:1
canceled;
theorem :: CARD_5:2
canceled;
theorem :: CARD_5:3
canceled;
theorem :: CARD_5:4
canceled;
theorem :: CARD_5:5
canceled;
theorem :: CARD_5:6
canceled;
theorem :: CARD_5:7
canceled;
theorem :: CARD_5:8
canceled;
theorem Th9: :: CARD_5:9
theorem Th10: :: CARD_5:10
theorem Th11: :: CARD_5:11
theorem Th12: :: CARD_5:12
theorem :: CARD_5:13
canceled;
theorem Th14: :: CARD_5:14
theorem Th15: :: CARD_5:15
theorem Th16: :: CARD_5:16
theorem Th17: :: CARD_5:17
theorem Th18: :: CARD_5:18
Lm2:
for phi, psi being Ordinal-Sequence st rng phi = rng psi & phi is increasing & psi is increasing holds
for A being Ordinal st A in dom phi holds
( A in dom psi & phi . A = psi . A )
theorem :: CARD_5:19
theorem Th20: :: CARD_5:20
theorem Th21: :: CARD_5:21
theorem :: CARD_5:22
theorem Th23: :: CARD_5:23
:: deftheorem CARD_5:def 1 :
canceled;
:: deftheorem Def2 defines cf CARD_5:def 2 :
:: deftheorem Def3 defines -powerfunc_of CARD_5:def 3 :
theorem :: CARD_5:24
theorem Th25: :: CARD_5:25
theorem Th26: :: CARD_5:26
theorem Th27: :: CARD_5:27
theorem :: CARD_5:28
theorem :: CARD_5:29
canceled;
theorem :: CARD_5:30
canceled;
theorem Th31: :: CARD_5:31
theorem :: CARD_5:32
:: deftheorem defines regular CARD_5:def 4 :
theorem :: CARD_5:33
canceled;
theorem Th34: :: CARD_5:34
Lm4:
1 = card 1
by CARD_1:def 5;
theorem Th35: :: CARD_5:35
theorem Th36: :: CARD_5:36
theorem :: CARD_5:37
theorem Th38: :: CARD_5:38
theorem Th39: :: CARD_5:39
theorem Th40: :: CARD_5:40
theorem Th41: :: CARD_5:41
theorem :: CARD_5:42
theorem Th43: :: CARD_5:43
theorem :: CARD_5:44
theorem Th45: :: CARD_5:45
theorem :: CARD_5:46
theorem :: CARD_5:47