Step | Hyp | Ref
| Expression |
1 | | onelon 6390 |
. . . . . . . . . . . 12
β’ ((π§ β On β§ π¦ β π§) β π¦ β On) |
2 | | vex 3479 |
. . . . . . . . . . . . 13
β’ π§ β V |
3 | | onelss 6407 |
. . . . . . . . . . . . . 14
β’ (π§ β On β (π¦ β π§ β π¦ β π§)) |
4 | 3 | imp 408 |
. . . . . . . . . . . . 13
β’ ((π§ β On β§ π¦ β π§) β π¦ β π§) |
5 | | ssdomg 8996 |
. . . . . . . . . . . . 13
β’ (π§ β V β (π¦ β π§ β π¦ βΌ π§)) |
6 | 2, 4, 5 | mpsyl 68 |
. . . . . . . . . . . 12
β’ ((π§ β On β§ π¦ β π§) β π¦ βΌ π§) |
7 | 1, 6 | jca 513 |
. . . . . . . . . . 11
β’ ((π§ β On β§ π¦ β π§) β (π¦ β On β§ π¦ βΌ π§)) |
8 | | domtr 9003 |
. . . . . . . . . . . . 13
β’ ((π¦ βΌ π§ β§ π§ βΌ π΄) β π¦ βΌ π΄) |
9 | 8 | anim2i 618 |
. . . . . . . . . . . 12
β’ ((π¦ β On β§ (π¦ βΌ π§ β§ π§ βΌ π΄)) β (π¦ β On β§ π¦ βΌ π΄)) |
10 | 9 | anassrs 469 |
. . . . . . . . . . 11
β’ (((π¦ β On β§ π¦ βΌ π§) β§ π§ βΌ π΄) β (π¦ β On β§ π¦ βΌ π΄)) |
11 | 7, 10 | sylan 581 |
. . . . . . . . . 10
β’ (((π§ β On β§ π¦ β π§) β§ π§ βΌ π΄) β (π¦ β On β§ π¦ βΌ π΄)) |
12 | 11 | exp31 421 |
. . . . . . . . 9
β’ (π§ β On β (π¦ β π§ β (π§ βΌ π΄ β (π¦ β On β§ π¦ βΌ π΄)))) |
13 | 12 | com12 32 |
. . . . . . . 8
β’ (π¦ β π§ β (π§ β On β (π§ βΌ π΄ β (π¦ β On β§ π¦ βΌ π΄)))) |
14 | 13 | impd 412 |
. . . . . . 7
β’ (π¦ β π§ β ((π§ β On β§ π§ βΌ π΄) β (π¦ β On β§ π¦ βΌ π΄))) |
15 | | breq1 5152 |
. . . . . . . 8
β’ (π₯ = π§ β (π₯ βΌ π΄ β π§ βΌ π΄)) |
16 | 15 | elrab 3684 |
. . . . . . 7
β’ (π§ β {π₯ β On β£ π₯ βΌ π΄} β (π§ β On β§ π§ βΌ π΄)) |
17 | | breq1 5152 |
. . . . . . . 8
β’ (π₯ = π¦ β (π₯ βΌ π΄ β π¦ βΌ π΄)) |
18 | 17 | elrab 3684 |
. . . . . . 7
β’ (π¦ β {π₯ β On β£ π₯ βΌ π΄} β (π¦ β On β§ π¦ βΌ π΄)) |
19 | 14, 16, 18 | 3imtr4g 296 |
. . . . . 6
β’ (π¦ β π§ β (π§ β {π₯ β On β£ π₯ βΌ π΄} β π¦ β {π₯ β On β£ π₯ βΌ π΄})) |
20 | 19 | imp 408 |
. . . . 5
β’ ((π¦ β π§ β§ π§ β {π₯ β On β£ π₯ βΌ π΄}) β π¦ β {π₯ β On β£ π₯ βΌ π΄}) |
21 | 20 | gen2 1799 |
. . . 4
β’
βπ¦βπ§((π¦ β π§ β§ π§ β {π₯ β On β£ π₯ βΌ π΄}) β π¦ β {π₯ β On β£ π₯ βΌ π΄}) |
22 | | dftr2 5268 |
. . . 4
β’ (Tr
{π₯ β On β£ π₯ βΌ π΄} β βπ¦βπ§((π¦ β π§ β§ π§ β {π₯ β On β£ π₯ βΌ π΄}) β π¦ β {π₯ β On β£ π₯ βΌ π΄})) |
23 | 21, 22 | mpbir 230 |
. . 3
β’ Tr {π₯ β On β£ π₯ βΌ π΄} |
24 | | ssrab2 4078 |
. . 3
β’ {π₯ β On β£ π₯ βΌ π΄} β On |
25 | | ordon 7764 |
. . 3
β’ Ord
On |
26 | | trssord 6382 |
. . 3
β’ ((Tr
{π₯ β On β£ π₯ βΌ π΄} β§ {π₯ β On β£ π₯ βΌ π΄} β On β§ Ord On) β Ord {π₯ β On β£ π₯ βΌ π΄}) |
27 | 23, 24, 25, 26 | mp3an 1462 |
. 2
β’ Ord
{π₯ β On β£ π₯ βΌ π΄} |
28 | | elex 3493 |
. . . . . 6
β’ (π΄ β π β π΄ β V) |
29 | | canth2g 9131 |
. . . . . . . . 9
β’ (π΄ β V β π΄ βΊ π« π΄) |
30 | | domsdomtr 9112 |
. . . . . . . . 9
β’ ((π₯ βΌ π΄ β§ π΄ βΊ π« π΄) β π₯ βΊ π« π΄) |
31 | 29, 30 | sylan2 594 |
. . . . . . . 8
β’ ((π₯ βΌ π΄ β§ π΄ β V) β π₯ βΊ π« π΄) |
32 | 31 | expcom 415 |
. . . . . . 7
β’ (π΄ β V β (π₯ βΌ π΄ β π₯ βΊ π« π΄)) |
33 | 32 | ralrimivw 3151 |
. . . . . 6
β’ (π΄ β V β βπ₯ β On (π₯ βΌ π΄ β π₯ βΊ π« π΄)) |
34 | 28, 33 | syl 17 |
. . . . 5
β’ (π΄ β π β βπ₯ β On (π₯ βΌ π΄ β π₯ βΊ π« π΄)) |
35 | | ss2rab 4069 |
. . . . 5
β’ ({π₯ β On β£ π₯ βΌ π΄} β {π₯ β On β£ π₯ βΊ π« π΄} β βπ₯ β On (π₯ βΌ π΄ β π₯ βΊ π« π΄)) |
36 | 34, 35 | sylibr 233 |
. . . 4
β’ (π΄ β π β {π₯ β On β£ π₯ βΌ π΄} β {π₯ β On β£ π₯ βΊ π« π΄}) |
37 | | pwexg 5377 |
. . . . . 6
β’ (π΄ β π β π« π΄ β V) |
38 | | numth3 10465 |
. . . . . 6
β’
(π« π΄ β
V β π« π΄ β
dom card) |
39 | | cardval2 9986 |
. . . . . 6
β’
(π« π΄ β
dom card β (cardβπ« π΄) = {π₯ β On β£ π₯ βΊ π« π΄}) |
40 | 37, 38, 39 | 3syl 18 |
. . . . 5
β’ (π΄ β π β (cardβπ« π΄) = {π₯ β On β£ π₯ βΊ π« π΄}) |
41 | | fvex 6905 |
. . . . 5
β’
(cardβπ« π΄) β V |
42 | 40, 41 | eqeltrrdi 2843 |
. . . 4
β’ (π΄ β π β {π₯ β On β£ π₯ βΊ π« π΄} β V) |
43 | | ssexg 5324 |
. . . 4
β’ (({π₯ β On β£ π₯ βΌ π΄} β {π₯ β On β£ π₯ βΊ π« π΄} β§ {π₯ β On β£ π₯ βΊ π« π΄} β V) β {π₯ β On β£ π₯ βΌ π΄} β V) |
44 | 36, 42, 43 | syl2anc 585 |
. . 3
β’ (π΄ β π β {π₯ β On β£ π₯ βΌ π΄} β V) |
45 | | elong 6373 |
. . 3
β’ ({π₯ β On β£ π₯ βΌ π΄} β V β ({π₯ β On β£ π₯ βΌ π΄} β On β Ord {π₯ β On β£ π₯ βΌ π΄})) |
46 | 44, 45 | syl 17 |
. 2
β’ (π΄ β π β ({π₯ β On β£ π₯ βΌ π΄} β On β Ord {π₯ β On β£ π₯ βΌ π΄})) |
47 | 27, 46 | mpbiri 258 |
1
β’ (π΄ β π β {π₯ β On β£ π₯ βΌ π΄} β On) |