Step | Hyp | Ref
| Expression |
1 | | limuni2 6384 |
. 2
β’ (Lim
(rankβ(π΄ Γ
π΅)) β Lim βͺ (rankβ(π΄ Γ π΅))) |
2 | | 0ellim 6385 |
. . . 4
β’ (Lim
βͺ (rankβ(π΄ Γ π΅)) β β
β βͺ (rankβ(π΄ Γ π΅))) |
3 | | n0i 4298 |
. . . 4
β’ (β
β βͺ (rankβ(π΄ Γ π΅)) β Β¬ βͺ
(rankβ(π΄ Γ
π΅)) =
β
) |
4 | | unieq 4881 |
. . . . . 6
β’
((rankβ(π΄
Γ π΅)) = β
β βͺ (rankβ(π΄ Γ π΅)) = βͺ
β
) |
5 | | uni0 4901 |
. . . . . 6
β’ βͺ β
= β
|
6 | 4, 5 | eqtrdi 2793 |
. . . . 5
β’
((rankβ(π΄
Γ π΅)) = β
β βͺ (rankβ(π΄ Γ π΅)) = β
) |
7 | 6 | con3i 154 |
. . . 4
β’ (Β¬
βͺ (rankβ(π΄ Γ π΅)) = β
β Β¬ (rankβ(π΄ Γ π΅)) = β
) |
8 | 2, 3, 7 | 3syl 18 |
. . 3
β’ (Lim
βͺ (rankβ(π΄ Γ π΅)) β Β¬ (rankβ(π΄ Γ π΅)) = β
) |
9 | | rankon 9738 |
. . . . . . . . . 10
β’
(rankβ(π΄ βͺ
π΅)) β
On |
10 | 9 | onsuci 7779 |
. . . . . . . . 9
β’ suc
(rankβ(π΄ βͺ π΅)) β On |
11 | 10 | onsuci 7779 |
. . . . . . . 8
β’ suc suc
(rankβ(π΄ βͺ π΅)) β On |
12 | 11 | elexi 3467 |
. . . . . . 7
β’ suc suc
(rankβ(π΄ βͺ π΅)) β V |
13 | 12 | sucid 6404 |
. . . . . 6
β’ suc suc
(rankβ(π΄ βͺ π΅)) β suc suc suc
(rankβ(π΄ βͺ π΅)) |
14 | 11 | onsuci 7779 |
. . . . . . . 8
β’ suc suc
suc (rankβ(π΄ βͺ
π΅)) β
On |
15 | | ontri1 6356 |
. . . . . . . 8
β’ ((suc suc
suc (rankβ(π΄ βͺ
π΅)) β On β§ suc suc
(rankβ(π΄ βͺ π΅)) β On) β (suc suc
suc (rankβ(π΄ βͺ
π΅)) β suc suc
(rankβ(π΄ βͺ π΅)) β Β¬ suc suc
(rankβ(π΄ βͺ π΅)) β suc suc suc
(rankβ(π΄ βͺ π΅)))) |
16 | 14, 11, 15 | mp2an 691 |
. . . . . . 7
β’ (suc suc
suc (rankβ(π΄ βͺ
π΅)) β suc suc
(rankβ(π΄ βͺ π΅)) β Β¬ suc suc
(rankβ(π΄ βͺ π΅)) β suc suc suc
(rankβ(π΄ βͺ π΅))) |
17 | 16 | con2bii 358 |
. . . . . 6
β’ (suc suc
(rankβ(π΄ βͺ π΅)) β suc suc suc
(rankβ(π΄ βͺ π΅)) β Β¬ suc suc suc
(rankβ(π΄ βͺ π΅)) β suc suc
(rankβ(π΄ βͺ π΅))) |
18 | 13, 17 | mpbi 229 |
. . . . 5
β’ Β¬
suc suc suc (rankβ(π΄
βͺ π΅)) β suc suc
(rankβ(π΄ βͺ π΅)) |
19 | | rankxplim.1 |
. . . . . . 7
β’ π΄ β V |
20 | | rankxplim.2 |
. . . . . . 7
β’ π΅ β V |
21 | 19, 20 | rankxpu 9819 |
. . . . . 6
β’
(rankβ(π΄
Γ π΅)) β suc suc
(rankβ(π΄ βͺ π΅)) |
22 | | sstr 3957 |
. . . . . 6
β’ ((suc suc
suc (rankβ(π΄ βͺ
π΅)) β
(rankβ(π΄ Γ
π΅)) β§
(rankβ(π΄ Γ
π΅)) β suc suc
(rankβ(π΄ βͺ π΅))) β suc suc suc
(rankβ(π΄ βͺ π΅)) β suc suc
(rankβ(π΄ βͺ π΅))) |
23 | 21, 22 | mpan2 690 |
. . . . 5
β’ (suc suc
suc (rankβ(π΄ βͺ
π΅)) β
(rankβ(π΄ Γ
π΅)) β suc suc suc
(rankβ(π΄ βͺ π΅)) β suc suc
(rankβ(π΄ βͺ π΅))) |
24 | 18, 23 | mto 196 |
. . . 4
β’ Β¬
suc suc suc (rankβ(π΄
βͺ π΅)) β
(rankβ(π΄ Γ
π΅)) |
25 | | reeanv 3220 |
. . . . 5
β’
(βπ₯ β On
βπ¦ β On
((rankβ(π΄ βͺ π΅)) = suc π₯ β§ (rankβ(π΄ Γ π΅)) = suc π¦) β (βπ₯ β On (rankβ(π΄ βͺ π΅)) = suc π₯ β§ βπ¦ β On (rankβ(π΄ Γ π΅)) = suc π¦)) |
26 | | simprl 770 |
. . . . . . . . . . . . 13
β’ ((Lim
βͺ (rankβ(π΄ Γ π΅)) β§ ((rankβ(π΄ βͺ π΅)) = suc π₯ β§ (rankβ(π΄ Γ π΅)) = suc π¦)) β (rankβ(π΄ βͺ π΅)) = suc π₯) |
27 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ ((Lim
βͺ (rankβ(π΄ Γ π΅)) β§ (rankβ(π΄ βͺ π΅)) = suc π₯) β (rankβ(π΄ βͺ π΅)) = suc π₯) |
28 | | df-ne 2945 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π΄ Γ π΅) β β
β Β¬ (π΄ Γ π΅) = β
) |
29 | 19, 20 | xpex 7692 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π΄ Γ π΅) β V |
30 | 29 | rankeq0 9804 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π΄ Γ π΅) = β
β (rankβ(π΄ Γ π΅)) = β
) |
31 | 30 | notbii 320 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (Β¬
(π΄ Γ π΅) = β
β Β¬
(rankβ(π΄ Γ
π΅)) =
β
) |
32 | 28, 31 | bitr2i 276 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (Β¬
(rankβ(π΄ Γ
π΅)) = β
β (π΄ Γ π΅) β β
) |
33 | 8, 32 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (Lim
βͺ (rankβ(π΄ Γ π΅)) β (π΄ Γ π΅) β β
) |
34 | | unixp 6239 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π΄ Γ π΅) β β
β βͺ βͺ (π΄ Γ π΅) = (π΄ βͺ π΅)) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (Lim
βͺ (rankβ(π΄ Γ π΅)) β βͺ βͺ (π΄
Γ π΅) = (π΄ βͺ π΅)) |
36 | 35 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (Lim
βͺ (rankβ(π΄ Γ π΅)) β (rankββͺ βͺ (π΄ Γ π΅)) = (rankβ(π΄ βͺ π΅))) |
37 | | rankuni 9806 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(rankββͺ βͺ
(π΄ Γ π΅)) = βͺ (rankββͺ (π΄ Γ π΅)) |
38 | | rankuni 9806 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(rankββͺ (π΄ Γ π΅)) = βͺ
(rankβ(π΄ Γ
π΅)) |
39 | 38 | unieqi 4883 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ βͺ (rankββͺ (π΄ Γ π΅)) = βͺ βͺ (rankβ(π΄ Γ π΅)) |
40 | 37, 39 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(rankββͺ βͺ
(π΄ Γ π΅)) = βͺ βͺ (rankβ(π΄ Γ π΅)) |
41 | 36, 40 | eqtr3di 2792 |
. . . . . . . . . . . . . . . . . . . 20
β’ (Lim
βͺ (rankβ(π΄ Γ π΅)) β (rankβ(π΄ βͺ π΅)) = βͺ βͺ (rankβ(π΄ Γ π΅))) |
42 | | eqimss 4005 |
. . . . . . . . . . . . . . . . . . . 20
β’
((rankβ(π΄
βͺ π΅)) = βͺ βͺ (rankβ(π΄ Γ π΅)) β (rankβ(π΄ βͺ π΅)) β βͺ
βͺ (rankβ(π΄ Γ π΅))) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (Lim
βͺ (rankβ(π΄ Γ π΅)) β (rankβ(π΄ βͺ π΅)) β βͺ
βͺ (rankβ(π΄ Γ π΅))) |
44 | 43 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((Lim
βͺ (rankβ(π΄ Γ π΅)) β§ (rankβ(π΄ βͺ π΅)) = suc π₯) β (rankβ(π΄ βͺ π΅)) β βͺ
βͺ (rankβ(π΄ Γ π΅))) |
45 | 27, 44 | eqsstrrd 3988 |
. . . . . . . . . . . . . . . . 17
β’ ((Lim
βͺ (rankβ(π΄ Γ π΅)) β§ (rankβ(π΄ βͺ π΅)) = suc π₯) β suc π₯ β βͺ βͺ (rankβ(π΄ Γ π΅))) |
46 | 45 | adantrr 716 |
. . . . . . . . . . . . . . . 16
β’ ((Lim
βͺ (rankβ(π΄ Γ π΅)) β§ ((rankβ(π΄ βͺ π΅)) = suc π₯ β§ (rankβ(π΄ Γ π΅)) = suc π¦)) β suc π₯ β βͺ βͺ (rankβ(π΄ Γ π΅))) |
47 | | limuni 6383 |
. . . . . . . . . . . . . . . . 17
β’ (Lim
βͺ (rankβ(π΄ Γ π΅)) β βͺ
(rankβ(π΄ Γ
π΅)) = βͺ βͺ (rankβ(π΄ Γ π΅))) |
48 | 47 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((Lim
βͺ (rankβ(π΄ Γ π΅)) β§ ((rankβ(π΄ βͺ π΅)) = suc π₯ β§ (rankβ(π΄ Γ π΅)) = suc π¦)) β βͺ
(rankβ(π΄ Γ
π΅)) = βͺ βͺ (rankβ(π΄ Γ π΅))) |
49 | 46, 48 | sseqtrrd 3990 |
. . . . . . . . . . . . . . 15
β’ ((Lim
βͺ (rankβ(π΄ Γ π΅)) β§ ((rankβ(π΄ βͺ π΅)) = suc π₯ β§ (rankβ(π΄ Γ π΅)) = suc π¦)) β suc π₯ β βͺ
(rankβ(π΄ Γ
π΅))) |
50 | | vex 3452 |
. . . . . . . . . . . . . . . 16
β’ π₯ β V |
51 | | rankon 9738 |
. . . . . . . . . . . . . . . . . 18
β’
(rankβ(π΄
Γ π΅)) β
On |
52 | 51 | onordi 6433 |
. . . . . . . . . . . . . . . . 17
β’ Ord
(rankβ(π΄ Γ
π΅)) |
53 | | orduni 7729 |
. . . . . . . . . . . . . . . . 17
β’ (Ord
(rankβ(π΄ Γ
π΅)) β Ord βͺ (rankβ(π΄ Γ π΅))) |
54 | 52, 53 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’ Ord βͺ (rankβ(π΄ Γ π΅)) |
55 | | ordelsuc 7760 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β V β§ Ord βͺ (rankβ(π΄ Γ π΅))) β (π₯ β βͺ
(rankβ(π΄ Γ
π΅)) β suc π₯ β βͺ (rankβ(π΄ Γ π΅)))) |
56 | 50, 54, 55 | mp2an 691 |
. . . . . . . . . . . . . . 15
β’ (π₯ β βͺ (rankβ(π΄ Γ π΅)) β suc π₯ β βͺ
(rankβ(π΄ Γ
π΅))) |
57 | 49, 56 | sylibr 233 |
. . . . . . . . . . . . . 14
β’ ((Lim
βͺ (rankβ(π΄ Γ π΅)) β§ ((rankβ(π΄ βͺ π΅)) = suc π₯ β§ (rankβ(π΄ Γ π΅)) = suc π¦)) β π₯ β βͺ
(rankβ(π΄ Γ
π΅))) |
58 | | limsuc 7790 |
. . . . . . . . . . . . . . 15
β’ (Lim
βͺ (rankβ(π΄ Γ π΅)) β (π₯ β βͺ
(rankβ(π΄ Γ
π΅)) β suc π₯ β βͺ (rankβ(π΄ Γ π΅)))) |
59 | 58 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((Lim
βͺ (rankβ(π΄ Γ π΅)) β§ ((rankβ(π΄ βͺ π΅)) = suc π₯ β§ (rankβ(π΄ Γ π΅)) = suc π¦)) β (π₯ β βͺ
(rankβ(π΄ Γ
π΅)) β suc π₯ β βͺ (rankβ(π΄ Γ π΅)))) |
60 | 57, 59 | mpbid 231 |
. . . . . . . . . . . . 13
β’ ((Lim
βͺ (rankβ(π΄ Γ π΅)) β§ ((rankβ(π΄ βͺ π΅)) = suc π₯ β§ (rankβ(π΄ Γ π΅)) = suc π¦)) β suc π₯ β βͺ
(rankβ(π΄ Γ
π΅))) |
61 | 26, 60 | eqeltrd 2838 |
. . . . . . . . . . . 12
β’ ((Lim
βͺ (rankβ(π΄ Γ π΅)) β§ ((rankβ(π΄ βͺ π΅)) = suc π₯ β§ (rankβ(π΄ Γ π΅)) = suc π¦)) β (rankβ(π΄ βͺ π΅)) β βͺ
(rankβ(π΄ Γ
π΅))) |
62 | | limsuc 7790 |
. . . . . . . . . . . . 13
β’ (Lim
βͺ (rankβ(π΄ Γ π΅)) β ((rankβ(π΄ βͺ π΅)) β βͺ
(rankβ(π΄ Γ
π΅)) β suc
(rankβ(π΄ βͺ π΅)) β βͺ (rankβ(π΄ Γ π΅)))) |
63 | 62 | adantr 482 |
. . . . . . . . . . . 12
β’ ((Lim
βͺ (rankβ(π΄ Γ π΅)) β§ ((rankβ(π΄ βͺ π΅)) = suc π₯ β§ (rankβ(π΄ Γ π΅)) = suc π¦)) β ((rankβ(π΄ βͺ π΅)) β βͺ
(rankβ(π΄ Γ
π΅)) β suc
(rankβ(π΄ βͺ π΅)) β βͺ (rankβ(π΄ Γ π΅)))) |
64 | 61, 63 | mpbid 231 |
. . . . . . . . . . 11
β’ ((Lim
βͺ (rankβ(π΄ Γ π΅)) β§ ((rankβ(π΄ βͺ π΅)) = suc π₯ β§ (rankβ(π΄ Γ π΅)) = suc π¦)) β suc (rankβ(π΄ βͺ π΅)) β βͺ
(rankβ(π΄ Γ
π΅))) |
65 | | ordsucelsuc 7762 |
. . . . . . . . . . . 12
β’ (Ord
βͺ (rankβ(π΄ Γ π΅)) β (suc (rankβ(π΄ βͺ π΅)) β βͺ
(rankβ(π΄ Γ
π΅)) β suc suc
(rankβ(π΄ βͺ π΅)) β suc βͺ (rankβ(π΄ Γ π΅)))) |
66 | 54, 65 | ax-mp 5 |
. . . . . . . . . . 11
β’ (suc
(rankβ(π΄ βͺ π΅)) β βͺ (rankβ(π΄ Γ π΅)) β suc suc (rankβ(π΄ βͺ π΅)) β suc βͺ
(rankβ(π΄ Γ
π΅))) |
67 | 64, 66 | sylib 217 |
. . . . . . . . . 10
β’ ((Lim
βͺ (rankβ(π΄ Γ π΅)) β§ ((rankβ(π΄ βͺ π΅)) = suc π₯ β§ (rankβ(π΄ Γ π΅)) = suc π¦)) β suc suc (rankβ(π΄ βͺ π΅)) β suc βͺ
(rankβ(π΄ Γ
π΅))) |
68 | | onsucuni2 7774 |
. . . . . . . . . . . 12
β’
(((rankβ(π΄
Γ π΅)) β On β§
(rankβ(π΄ Γ
π΅)) = suc π¦) β suc βͺ (rankβ(π΄ Γ π΅)) = (rankβ(π΄ Γ π΅))) |
69 | 51, 68 | mpan 689 |
. . . . . . . . . . 11
β’
((rankβ(π΄
Γ π΅)) = suc π¦ β suc βͺ (rankβ(π΄ Γ π΅)) = (rankβ(π΄ Γ π΅))) |
70 | 69 | ad2antll 728 |
. . . . . . . . . 10
β’ ((Lim
βͺ (rankβ(π΄ Γ π΅)) β§ ((rankβ(π΄ βͺ π΅)) = suc π₯ β§ (rankβ(π΄ Γ π΅)) = suc π¦)) β suc βͺ
(rankβ(π΄ Γ
π΅)) = (rankβ(π΄ Γ π΅))) |
71 | 67, 70 | eleqtrd 2840 |
. . . . . . . . 9
β’ ((Lim
βͺ (rankβ(π΄ Γ π΅)) β§ ((rankβ(π΄ βͺ π΅)) = suc π₯ β§ (rankβ(π΄ Γ π΅)) = suc π¦)) β suc suc (rankβ(π΄ βͺ π΅)) β (rankβ(π΄ Γ π΅))) |
72 | 11, 51 | onsucssi 7782 |
. . . . . . . . 9
β’ (suc suc
(rankβ(π΄ βͺ π΅)) β (rankβ(π΄ Γ π΅)) β suc suc suc (rankβ(π΄ βͺ π΅)) β (rankβ(π΄ Γ π΅))) |
73 | 71, 72 | sylib 217 |
. . . . . . . 8
β’ ((Lim
βͺ (rankβ(π΄ Γ π΅)) β§ ((rankβ(π΄ βͺ π΅)) = suc π₯ β§ (rankβ(π΄ Γ π΅)) = suc π¦)) β suc suc suc (rankβ(π΄ βͺ π΅)) β (rankβ(π΄ Γ π΅))) |
74 | 73 | ex 414 |
. . . . . . 7
β’ (Lim
βͺ (rankβ(π΄ Γ π΅)) β (((rankβ(π΄ βͺ π΅)) = suc π₯ β§ (rankβ(π΄ Γ π΅)) = suc π¦) β suc suc suc (rankβ(π΄ βͺ π΅)) β (rankβ(π΄ Γ π΅)))) |
75 | 74 | a1d 25 |
. . . . . 6
β’ (Lim
βͺ (rankβ(π΄ Γ π΅)) β ((π₯ β On β§ π¦ β On) β (((rankβ(π΄ βͺ π΅)) = suc π₯ β§ (rankβ(π΄ Γ π΅)) = suc π¦) β suc suc suc (rankβ(π΄ βͺ π΅)) β (rankβ(π΄ Γ π΅))))) |
76 | 75 | rexlimdvv 3205 |
. . . . 5
β’ (Lim
βͺ (rankβ(π΄ Γ π΅)) β (βπ₯ β On βπ¦ β On ((rankβ(π΄ βͺ π΅)) = suc π₯ β§ (rankβ(π΄ Γ π΅)) = suc π¦) β suc suc suc (rankβ(π΄ βͺ π΅)) β (rankβ(π΄ Γ π΅)))) |
77 | 25, 76 | biimtrrid 242 |
. . . 4
β’ (Lim
βͺ (rankβ(π΄ Γ π΅)) β ((βπ₯ β On (rankβ(π΄ βͺ π΅)) = suc π₯ β§ βπ¦ β On (rankβ(π΄ Γ π΅)) = suc π¦) β suc suc suc (rankβ(π΄ βͺ π΅)) β (rankβ(π΄ Γ π΅)))) |
78 | 24, 77 | mtoi 198 |
. . 3
β’ (Lim
βͺ (rankβ(π΄ Γ π΅)) β Β¬ (βπ₯ β On (rankβ(π΄ βͺ π΅)) = suc π₯ β§ βπ¦ β On (rankβ(π΄ Γ π΅)) = suc π¦)) |
79 | | ianor 981 |
. . . . . 6
β’ (Β¬
(βπ₯ β On
(rankβ(π΄ βͺ π΅)) = suc π₯ β§ βπ¦ β On (rankβ(π΄ Γ π΅)) = suc π¦) β (Β¬ βπ₯ β On (rankβ(π΄ βͺ π΅)) = suc π₯ β¨ Β¬ βπ¦ β On (rankβ(π΄ Γ π΅)) = suc π¦)) |
80 | | un00 4407 |
. . . . . . . . . . . . . 14
β’ ((π΄ = β
β§ π΅ = β
) β (π΄ βͺ π΅) = β
) |
81 | | animorl 977 |
. . . . . . . . . . . . . 14
β’ ((π΄ = β
β§ π΅ = β
) β (π΄ = β
β¨ π΅ = β
)) |
82 | 80, 81 | sylbir 234 |
. . . . . . . . . . . . 13
β’ ((π΄ βͺ π΅) = β
β (π΄ = β
β¨ π΅ = β
)) |
83 | | xpeq0 6117 |
. . . . . . . . . . . . 13
β’ ((π΄ Γ π΅) = β
β (π΄ = β
β¨ π΅ = β
)) |
84 | 82, 83 | sylibr 233 |
. . . . . . . . . . . 12
β’ ((π΄ βͺ π΅) = β
β (π΄ Γ π΅) = β
) |
85 | 84 | con3i 154 |
. . . . . . . . . . 11
β’ (Β¬
(π΄ Γ π΅) = β
β Β¬ (π΄ βͺ π΅) = β
) |
86 | 31, 85 | sylbir 234 |
. . . . . . . . . 10
β’ (Β¬
(rankβ(π΄ Γ
π΅)) = β
β Β¬
(π΄ βͺ π΅) = β
) |
87 | 19, 20 | unex 7685 |
. . . . . . . . . . . 12
β’ (π΄ βͺ π΅) β V |
88 | 87 | rankeq0 9804 |
. . . . . . . . . . 11
β’ ((π΄ βͺ π΅) = β
β (rankβ(π΄ βͺ π΅)) = β
) |
89 | 88 | notbii 320 |
. . . . . . . . . 10
β’ (Β¬
(π΄ βͺ π΅) = β
β Β¬ (rankβ(π΄ βͺ π΅)) = β
) |
90 | 86, 89 | sylib 217 |
. . . . . . . . 9
β’ (Β¬
(rankβ(π΄ Γ
π΅)) = β
β Β¬
(rankβ(π΄ βͺ π΅)) = β
) |
91 | 9 | onordi 6433 |
. . . . . . . . . . 11
β’ Ord
(rankβ(π΄ βͺ π΅)) |
92 | | ordzsl 7786 |
. . . . . . . . . . 11
β’ (Ord
(rankβ(π΄ βͺ π΅)) β ((rankβ(π΄ βͺ π΅)) = β
β¨ βπ₯ β On (rankβ(π΄ βͺ π΅)) = suc π₯ β¨ Lim (rankβ(π΄ βͺ π΅)))) |
93 | 91, 92 | mpbi 229 |
. . . . . . . . . 10
β’
((rankβ(π΄
βͺ π΅)) = β
β¨
βπ₯ β On
(rankβ(π΄ βͺ π΅)) = suc π₯ β¨ Lim (rankβ(π΄ βͺ π΅))) |
94 | 93 | 3ori 1425 |
. . . . . . . . 9
β’ ((Β¬
(rankβ(π΄ βͺ π΅)) = β
β§ Β¬
βπ₯ β On
(rankβ(π΄ βͺ π΅)) = suc π₯) β Lim (rankβ(π΄ βͺ π΅))) |
95 | 90, 94 | sylan 581 |
. . . . . . . 8
β’ ((Β¬
(rankβ(π΄ Γ
π΅)) = β
β§ Β¬
βπ₯ β On
(rankβ(π΄ βͺ π΅)) = suc π₯) β Lim (rankβ(π΄ βͺ π΅))) |
96 | 95 | ex 414 |
. . . . . . 7
β’ (Β¬
(rankβ(π΄ Γ
π΅)) = β
β (Β¬
βπ₯ β On
(rankβ(π΄ βͺ π΅)) = suc π₯ β Lim (rankβ(π΄ βͺ π΅)))) |
97 | | ordzsl 7786 |
. . . . . . . . . 10
β’ (Ord
(rankβ(π΄ Γ
π΅)) β
((rankβ(π΄ Γ
π΅)) = β
β¨
βπ¦ β On
(rankβ(π΄ Γ
π΅)) = suc π¦ β¨ Lim (rankβ(π΄ Γ π΅)))) |
98 | 52, 97 | mpbi 229 |
. . . . . . . . 9
β’
((rankβ(π΄
Γ π΅)) = β
β¨
βπ¦ β On
(rankβ(π΄ Γ
π΅)) = suc π¦ β¨ Lim (rankβ(π΄ Γ π΅))) |
99 | 98 | 3ori 1425 |
. . . . . . . 8
β’ ((Β¬
(rankβ(π΄ Γ
π΅)) = β
β§ Β¬
βπ¦ β On
(rankβ(π΄ Γ
π΅)) = suc π¦) β Lim (rankβ(π΄ Γ π΅))) |
100 | 99 | ex 414 |
. . . . . . 7
β’ (Β¬
(rankβ(π΄ Γ
π΅)) = β
β (Β¬
βπ¦ β On
(rankβ(π΄ Γ
π΅)) = suc π¦ β Lim (rankβ(π΄ Γ π΅)))) |
101 | 96, 100 | orim12d 964 |
. . . . . 6
β’ (Β¬
(rankβ(π΄ Γ
π΅)) = β
β
((Β¬ βπ₯ β On
(rankβ(π΄ βͺ π΅)) = suc π₯ β¨ Β¬ βπ¦ β On (rankβ(π΄ Γ π΅)) = suc π¦) β (Lim (rankβ(π΄ βͺ π΅)) β¨ Lim (rankβ(π΄ Γ π΅))))) |
102 | 79, 101 | biimtrid 241 |
. . . . 5
β’ (Β¬
(rankβ(π΄ Γ
π΅)) = β
β (Β¬
(βπ₯ β On
(rankβ(π΄ βͺ π΅)) = suc π₯ β§ βπ¦ β On (rankβ(π΄ Γ π΅)) = suc π¦) β (Lim (rankβ(π΄ βͺ π΅)) β¨ Lim (rankβ(π΄ Γ π΅))))) |
103 | 102 | imp 408 |
. . . 4
β’ ((Β¬
(rankβ(π΄ Γ
π΅)) = β
β§ Β¬
(βπ₯ β On
(rankβ(π΄ βͺ π΅)) = suc π₯ β§ βπ¦ β On (rankβ(π΄ Γ π΅)) = suc π¦)) β (Lim (rankβ(π΄ βͺ π΅)) β¨ Lim (rankβ(π΄ Γ π΅)))) |
104 | | simpl 484 |
. . . . . . . 8
β’ ((Lim
(rankβ(π΄ βͺ π΅)) β§ Β¬
(rankβ(π΄ Γ
π΅)) = β
) β Lim
(rankβ(π΄ βͺ π΅))) |
105 | 30 | necon3abii 2991 |
. . . . . . . . . 10
β’ ((π΄ Γ π΅) β β
β Β¬
(rankβ(π΄ Γ
π΅)) =
β
) |
106 | 19, 20 | rankxplim 9822 |
. . . . . . . . . 10
β’ ((Lim
(rankβ(π΄ βͺ π΅)) β§ (π΄ Γ π΅) β β
) β (rankβ(π΄ Γ π΅)) = (rankβ(π΄ βͺ π΅))) |
107 | 105, 106 | sylan2br 596 |
. . . . . . . . 9
β’ ((Lim
(rankβ(π΄ βͺ π΅)) β§ Β¬
(rankβ(π΄ Γ
π΅)) = β
) β
(rankβ(π΄ Γ
π΅)) = (rankβ(π΄ βͺ π΅))) |
108 | | limeq 6334 |
. . . . . . . . 9
β’
((rankβ(π΄
Γ π΅)) =
(rankβ(π΄ βͺ π΅)) β (Lim
(rankβ(π΄ Γ
π΅)) β Lim
(rankβ(π΄ βͺ π΅)))) |
109 | 107, 108 | syl 17 |
. . . . . . . 8
β’ ((Lim
(rankβ(π΄ βͺ π΅)) β§ Β¬
(rankβ(π΄ Γ
π΅)) = β
) β (Lim
(rankβ(π΄ Γ
π΅)) β Lim
(rankβ(π΄ βͺ π΅)))) |
110 | 104, 109 | mpbird 257 |
. . . . . . 7
β’ ((Lim
(rankβ(π΄ βͺ π΅)) β§ Β¬
(rankβ(π΄ Γ
π΅)) = β
) β Lim
(rankβ(π΄ Γ
π΅))) |
111 | 110 | expcom 415 |
. . . . . 6
β’ (Β¬
(rankβ(π΄ Γ
π΅)) = β
β (Lim
(rankβ(π΄ βͺ π΅)) β Lim (rankβ(π΄ Γ π΅)))) |
112 | | idd 24 |
. . . . . 6
β’ (Β¬
(rankβ(π΄ Γ
π΅)) = β
β (Lim
(rankβ(π΄ Γ
π΅)) β Lim
(rankβ(π΄ Γ
π΅)))) |
113 | 111, 112 | jaod 858 |
. . . . 5
β’ (Β¬
(rankβ(π΄ Γ
π΅)) = β
β ((Lim
(rankβ(π΄ βͺ π΅)) β¨ Lim (rankβ(π΄ Γ π΅))) β Lim (rankβ(π΄ Γ π΅)))) |
114 | 113 | adantr 482 |
. . . 4
β’ ((Β¬
(rankβ(π΄ Γ
π΅)) = β
β§ Β¬
(βπ₯ β On
(rankβ(π΄ βͺ π΅)) = suc π₯ β§ βπ¦ β On (rankβ(π΄ Γ π΅)) = suc π¦)) β ((Lim (rankβ(π΄ βͺ π΅)) β¨ Lim (rankβ(π΄ Γ π΅))) β Lim (rankβ(π΄ Γ π΅)))) |
115 | 103, 114 | mpd 15 |
. . 3
β’ ((Β¬
(rankβ(π΄ Γ
π΅)) = β
β§ Β¬
(βπ₯ β On
(rankβ(π΄ βͺ π΅)) = suc π₯ β§ βπ¦ β On (rankβ(π΄ Γ π΅)) = suc π¦)) β Lim (rankβ(π΄ Γ π΅))) |
116 | 8, 78, 115 | syl2anc 585 |
. 2
β’ (Lim
βͺ (rankβ(π΄ Γ π΅)) β Lim (rankβ(π΄ Γ π΅))) |
117 | 1, 116 | impbii 208 |
1
β’ (Lim
(rankβ(π΄ Γ
π΅)) β Lim βͺ (rankβ(π΄ Γ π΅))) |