Step | Hyp | Ref
| Expression |
1 | | r1tr 9720 |
. . 3
β’ Tr
(π
1βπ΄) |
2 | 1 | a1i 11 |
. 2
β’ ((π΄ β π β§ Lim π΄) β Tr
(π
1βπ΄)) |
3 | | limelon 6385 |
. . . . . 6
β’ ((π΄ β π β§ Lim π΄) β π΄ β On) |
4 | | r1fnon 9711 |
. . . . . . 7
β’
π
1 Fn On |
5 | 4 | fndmi 6610 |
. . . . . 6
β’ dom
π
1 = On |
6 | 3, 5 | eleqtrrdi 2845 |
. . . . 5
β’ ((π΄ β π β§ Lim π΄) β π΄ β dom
π
1) |
7 | | onssr1 9775 |
. . . . 5
β’ (π΄ β dom
π
1 β π΄ β (π
1βπ΄)) |
8 | 6, 7 | syl 17 |
. . . 4
β’ ((π΄ β π β§ Lim π΄) β π΄ β (π
1βπ΄)) |
9 | | 0ellim 6384 |
. . . . 5
β’ (Lim
π΄ β β
β
π΄) |
10 | 9 | adantl 483 |
. . . 4
β’ ((π΄ β π β§ Lim π΄) β β
β π΄) |
11 | 8, 10 | sseldd 3949 |
. . 3
β’ ((π΄ β π β§ Lim π΄) β β
β
(π
1βπ΄)) |
12 | 11 | ne0d 4299 |
. 2
β’ ((π΄ β π β§ Lim π΄) β (π
1βπ΄) β β
) |
13 | | rankuni 9807 |
. . . . . 6
β’
(rankββͺ π₯) = βͺ
(rankβπ₯) |
14 | | rankon 9739 |
. . . . . . . . 9
β’
(rankβπ₯)
β On |
15 | | eloni 6331 |
. . . . . . . . 9
β’
((rankβπ₯)
β On β Ord (rankβπ₯)) |
16 | | orduniss 6418 |
. . . . . . . . 9
β’ (Ord
(rankβπ₯) β βͺ (rankβπ₯) β (rankβπ₯)) |
17 | 14, 15, 16 | mp2b 10 |
. . . . . . . 8
β’ βͺ (rankβπ₯) β (rankβπ₯) |
18 | 17 | a1i 11 |
. . . . . . 7
β’ (((π΄ β π β§ Lim π΄) β§ π₯ β (π
1βπ΄)) β βͺ (rankβπ₯) β (rankβπ₯)) |
19 | | rankr1ai 9742 |
. . . . . . . 8
β’ (π₯ β
(π
1βπ΄) β (rankβπ₯) β π΄) |
20 | 19 | adantl 483 |
. . . . . . 7
β’ (((π΄ β π β§ Lim π΄) β§ π₯ β (π
1βπ΄)) β (rankβπ₯) β π΄) |
21 | | onuni 7727 |
. . . . . . . . 9
β’
((rankβπ₯)
β On β βͺ (rankβπ₯) β On) |
22 | 14, 21 | ax-mp 5 |
. . . . . . . 8
β’ βͺ (rankβπ₯) β On |
23 | 3 | adantr 482 |
. . . . . . . 8
β’ (((π΄ β π β§ Lim π΄) β§ π₯ β (π
1βπ΄)) β π΄ β On) |
24 | | ontr2 6368 |
. . . . . . . 8
β’ ((βͺ (rankβπ₯) β On β§ π΄ β On) β ((βͺ (rankβπ₯) β (rankβπ₯) β§ (rankβπ₯) β π΄) β βͺ
(rankβπ₯) β π΄)) |
25 | 22, 23, 24 | sylancr 588 |
. . . . . . 7
β’ (((π΄ β π β§ Lim π΄) β§ π₯ β (π
1βπ΄)) β ((βͺ (rankβπ₯) β (rankβπ₯) β§ (rankβπ₯) β π΄) β βͺ
(rankβπ₯) β π΄)) |
26 | 18, 20, 25 | mp2and 698 |
. . . . . 6
β’ (((π΄ β π β§ Lim π΄) β§ π₯ β (π
1βπ΄)) β βͺ (rankβπ₯) β π΄) |
27 | 13, 26 | eqeltrid 2838 |
. . . . 5
β’ (((π΄ β π β§ Lim π΄) β§ π₯ β (π
1βπ΄)) β (rankββͺ π₯)
β π΄) |
28 | | r1elwf 9740 |
. . . . . . . 8
β’ (π₯ β
(π
1βπ΄) β π₯ β βͺ
(π
1 β On)) |
29 | 28 | adantl 483 |
. . . . . . 7
β’ (((π΄ β π β§ Lim π΄) β§ π₯ β (π
1βπ΄)) β π₯ β βͺ
(π
1 β On)) |
30 | | uniwf 9763 |
. . . . . . 7
β’ (π₯ β βͺ (π
1 β On) β βͺ π₯
β βͺ (π
1 β
On)) |
31 | 29, 30 | sylib 217 |
. . . . . 6
β’ (((π΄ β π β§ Lim π΄) β§ π₯ β (π
1βπ΄)) β βͺ π₯
β βͺ (π
1 β
On)) |
32 | 6 | adantr 482 |
. . . . . 6
β’ (((π΄ β π β§ Lim π΄) β§ π₯ β (π
1βπ΄)) β π΄ β dom
π
1) |
33 | | rankr1ag 9746 |
. . . . . 6
β’ ((βͺ π₯
β βͺ (π
1 β On) β§
π΄ β dom
π
1) β (βͺ π₯ β (π
1βπ΄) β (rankββͺ π₯)
β π΄)) |
34 | 31, 32, 33 | syl2anc 585 |
. . . . 5
β’ (((π΄ β π β§ Lim π΄) β§ π₯ β (π
1βπ΄)) β (βͺ π₯
β (π
1βπ΄) β (rankββͺ π₯)
β π΄)) |
35 | 27, 34 | mpbird 257 |
. . . 4
β’ (((π΄ β π β§ Lim π΄) β§ π₯ β (π
1βπ΄)) β βͺ π₯
β (π
1βπ΄)) |
36 | | r1pwcl 9791 |
. . . . . 6
β’ (Lim
π΄ β (π₯ β
(π
1βπ΄) β π« π₯ β (π
1βπ΄))) |
37 | 36 | adantl 483 |
. . . . 5
β’ ((π΄ β π β§ Lim π΄) β (π₯ β (π
1βπ΄) β π« π₯ β
(π
1βπ΄))) |
38 | 37 | biimpa 478 |
. . . 4
β’ (((π΄ β π β§ Lim π΄) β§ π₯ β (π
1βπ΄)) β π« π₯ β
(π
1βπ΄)) |
39 | 28 | ad2antlr 726 |
. . . . . . . 8
β’ ((((π΄ β π β§ Lim π΄) β§ π₯ β (π
1βπ΄)) β§ π¦ β (π
1βπ΄)) β π₯ β βͺ
(π
1 β On)) |
40 | | r1elwf 9740 |
. . . . . . . . 9
β’ (π¦ β
(π
1βπ΄) β π¦ β βͺ
(π
1 β On)) |
41 | 40 | adantl 483 |
. . . . . . . 8
β’ ((((π΄ β π β§ Lim π΄) β§ π₯ β (π
1βπ΄)) β§ π¦ β (π
1βπ΄)) β π¦ β βͺ
(π
1 β On)) |
42 | | rankprb 9795 |
. . . . . . . 8
β’ ((π₯ β βͺ (π
1 β On) β§ π¦ β βͺ (π
1 β On)) β
(rankβ{π₯, π¦}) = suc ((rankβπ₯) βͺ (rankβπ¦))) |
43 | 39, 41, 42 | syl2anc 585 |
. . . . . . 7
β’ ((((π΄ β π β§ Lim π΄) β§ π₯ β (π
1βπ΄)) β§ π¦ β (π
1βπ΄)) β (rankβ{π₯, π¦}) = suc ((rankβπ₯) βͺ (rankβπ¦))) |
44 | | limord 6381 |
. . . . . . . . . 10
β’ (Lim
π΄ β Ord π΄) |
45 | 44 | ad3antlr 730 |
. . . . . . . . 9
β’ ((((π΄ β π β§ Lim π΄) β§ π₯ β (π
1βπ΄)) β§ π¦ β (π
1βπ΄)) β Ord π΄) |
46 | 20 | adantr 482 |
. . . . . . . . 9
β’ ((((π΄ β π β§ Lim π΄) β§ π₯ β (π
1βπ΄)) β§ π¦ β (π
1βπ΄)) β (rankβπ₯) β π΄) |
47 | | rankr1ai 9742 |
. . . . . . . . . 10
β’ (π¦ β
(π
1βπ΄) β (rankβπ¦) β π΄) |
48 | 47 | adantl 483 |
. . . . . . . . 9
β’ ((((π΄ β π β§ Lim π΄) β§ π₯ β (π
1βπ΄)) β§ π¦ β (π
1βπ΄)) β (rankβπ¦) β π΄) |
49 | | ordunel 7766 |
. . . . . . . . 9
β’ ((Ord
π΄ β§ (rankβπ₯) β π΄ β§ (rankβπ¦) β π΄) β ((rankβπ₯) βͺ (rankβπ¦)) β π΄) |
50 | 45, 46, 48, 49 | syl3anc 1372 |
. . . . . . . 8
β’ ((((π΄ β π β§ Lim π΄) β§ π₯ β (π
1βπ΄)) β§ π¦ β (π
1βπ΄)) β ((rankβπ₯) βͺ (rankβπ¦)) β π΄) |
51 | | limsuc 7789 |
. . . . . . . . 9
β’ (Lim
π΄ β
(((rankβπ₯) βͺ
(rankβπ¦)) β
π΄ β suc
((rankβπ₯) βͺ
(rankβπ¦)) β
π΄)) |
52 | 51 | ad3antlr 730 |
. . . . . . . 8
β’ ((((π΄ β π β§ Lim π΄) β§ π₯ β (π
1βπ΄)) β§ π¦ β (π
1βπ΄)) β (((rankβπ₯) βͺ (rankβπ¦)) β π΄ β suc ((rankβπ₯) βͺ (rankβπ¦)) β π΄)) |
53 | 50, 52 | mpbid 231 |
. . . . . . 7
β’ ((((π΄ β π β§ Lim π΄) β§ π₯ β (π
1βπ΄)) β§ π¦ β (π
1βπ΄)) β suc ((rankβπ₯) βͺ (rankβπ¦)) β π΄) |
54 | 43, 53 | eqeltrd 2834 |
. . . . . 6
β’ ((((π΄ β π β§ Lim π΄) β§ π₯ β (π
1βπ΄)) β§ π¦ β (π
1βπ΄)) β (rankβ{π₯, π¦}) β π΄) |
55 | | prwf 9755 |
. . . . . . . 8
β’ ((π₯ β βͺ (π
1 β On) β§ π¦ β βͺ (π
1 β On)) β {π₯, π¦} β βͺ
(π
1 β On)) |
56 | 39, 41, 55 | syl2anc 585 |
. . . . . . 7
β’ ((((π΄ β π β§ Lim π΄) β§ π₯ β (π
1βπ΄)) β§ π¦ β (π
1βπ΄)) β {π₯, π¦} β βͺ
(π
1 β On)) |
57 | 32 | adantr 482 |
. . . . . . 7
β’ ((((π΄ β π β§ Lim π΄) β§ π₯ β (π
1βπ΄)) β§ π¦ β (π
1βπ΄)) β π΄ β dom
π
1) |
58 | | rankr1ag 9746 |
. . . . . . 7
β’ (({π₯, π¦} β βͺ
(π
1 β On) β§ π΄ β dom π
1) β
({π₯, π¦} β (π
1βπ΄) β (rankβ{π₯, π¦}) β π΄)) |
59 | 56, 57, 58 | syl2anc 585 |
. . . . . 6
β’ ((((π΄ β π β§ Lim π΄) β§ π₯ β (π
1βπ΄)) β§ π¦ β (π
1βπ΄)) β ({π₯, π¦} β (π
1βπ΄) β (rankβ{π₯, π¦}) β π΄)) |
60 | 54, 59 | mpbird 257 |
. . . . 5
β’ ((((π΄ β π β§ Lim π΄) β§ π₯ β (π
1βπ΄)) β§ π¦ β (π
1βπ΄)) β {π₯, π¦} β (π
1βπ΄)) |
61 | 60 | ralrimiva 3140 |
. . . 4
β’ (((π΄ β π β§ Lim π΄) β§ π₯ β (π
1βπ΄)) β βπ¦ β
(π
1βπ΄){π₯, π¦} β (π
1βπ΄)) |
62 | 35, 38, 61 | 3jca 1129 |
. . 3
β’ (((π΄ β π β§ Lim π΄) β§ π₯ β (π
1βπ΄)) β (βͺ π₯
β (π
1βπ΄) β§ π« π₯ β (π
1βπ΄) β§ βπ¦ β
(π
1βπ΄){π₯, π¦} β (π
1βπ΄))) |
63 | 62 | ralrimiva 3140 |
. 2
β’ ((π΄ β π β§ Lim π΄) β βπ₯ β (π
1βπ΄)(βͺ
π₯ β
(π
1βπ΄) β§ π« π₯ β (π
1βπ΄) β§ βπ¦ β
(π
1βπ΄){π₯, π¦} β (π
1βπ΄))) |
64 | | fvex 6859 |
. . 3
β’
(π
1βπ΄) β V |
65 | | iswun 10648 |
. . 3
β’
((π
1βπ΄) β V β
((π
1βπ΄) β WUni β (Tr
(π
1βπ΄) β§ (π
1βπ΄) β β
β§
βπ₯ β
(π
1βπ΄)(βͺ π₯ β
(π
1βπ΄) β§ π« π₯ β (π
1βπ΄) β§ βπ¦ β
(π
1βπ΄){π₯, π¦} β (π
1βπ΄))))) |
66 | 64, 65 | ax-mp 5 |
. 2
β’
((π
1βπ΄) β WUni β (Tr
(π
1βπ΄) β§ (π
1βπ΄) β β
β§
βπ₯ β
(π
1βπ΄)(βͺ π₯ β
(π
1βπ΄) β§ π« π₯ β (π
1βπ΄) β§ βπ¦ β
(π
1βπ΄){π₯, π¦} β (π
1βπ΄)))) |
67 | 2, 12, 63, 66 | syl3anbrc 1344 |
1
β’ ((π΄ β π β§ Lim π΄) β (π
1βπ΄) β WUni) |