:: Mahlo and inaccessible cardinals
:: by Josef Urban
::
:: Received August 28, 2000
:: Copyright (c) 2000 Association of Mizar Users
:: deftheorem Def1 defines is_unbounded_in CARD_LAR:def 1 :
:: deftheorem Def2 defines is_closed_in CARD_LAR:def 2 :
:: deftheorem Def3 defines is_club_in CARD_LAR:def 3 :
:: deftheorem Def4 defines unbounded CARD_LAR:def 4 :
:: deftheorem Def5 defines closed CARD_LAR:def 5 :
theorem :: CARD_LAR:1
canceled;
theorem Th2: :: CARD_LAR:2
theorem Th3: :: CARD_LAR:3
theorem Th4: :: CARD_LAR:4
theorem Th5: :: CARD_LAR:5
theorem Th6: :: CARD_LAR:6
theorem Th7: :: CARD_LAR:7
theorem Th8: :: CARD_LAR:8
theorem Th9: :: CARD_LAR:9
:: deftheorem Def6 defines LBound CARD_LAR:def 6 :
theorem Th10: :: CARD_LAR:10
theorem Th11: :: CARD_LAR:11
theorem Th12: :: CARD_LAR:12
theorem Th13: :: CARD_LAR:13
:: deftheorem Def7 defines stationary CARD_LAR:def 7 :
theorem Th14: :: CARD_LAR:14
:: deftheorem Def8 defines is_stationary_in CARD_LAR:def 8 :
theorem :: CARD_LAR:15
theorem :: CARD_LAR:16
:: deftheorem defines limpoints CARD_LAR:def 9 :
theorem Th17: :: CARD_LAR:17
theorem :: CARD_LAR:18
theorem Th19: :: CARD_LAR:19
theorem Th20: :: CARD_LAR:20
theorem Th21: :: CARD_LAR:21
theorem Th22: :: CARD_LAR:22
theorem Th23: :: CARD_LAR:23
theorem :: CARD_LAR:24
theorem Th25: :: CARD_LAR:25
theorem :: CARD_LAR:26
:: deftheorem Def10 defines Mahlo CARD_LAR:def 10 :
:: deftheorem Def11 defines strongly_Mahlo CARD_LAR:def 11 :
theorem Th27: :: CARD_LAR:27
theorem Th28: :: CARD_LAR:28
theorem Th29: :: CARD_LAR:29
theorem :: CARD_LAR:30
theorem Th31: :: CARD_LAR:31
theorem :: CARD_LAR:32
theorem Th33: :: CARD_LAR:33
theorem Th34: :: CARD_LAR:34
deffunc H1( Ordinal) -> set = Rank $1;
theorem Th35: :: CARD_LAR:35
theorem Th36: :: CARD_LAR:36
theorem Th37: :: CARD_LAR:37
theorem Th38: :: CARD_LAR:38
theorem Th39: :: CARD_LAR:39
theorem :: CARD_LAR:40