Step | Hyp | Ref
| Expression |
1 | | cardon 9885 |
. . 3
β’
(cardβπ΄)
β On |
2 | | eleq1 2822 |
. . 3
β’
((cardβπ΄) =
π΄ β ((cardβπ΄) β On β π΄ β On)) |
3 | 1, 2 | mpbii 232 |
. 2
β’
((cardβπ΄) =
π΄ β π΄ β On) |
4 | | eqss 3960 |
. . . . 5
β’
((cardβπ΄) =
π΄ β ((cardβπ΄) β π΄ β§ π΄ β (cardβπ΄))) |
5 | | cardonle 9898 |
. . . . . 6
β’ (π΄ β On β
(cardβπ΄) β
π΄) |
6 | 5 | biantrurd 534 |
. . . . 5
β’ (π΄ β On β (π΄ β (cardβπ΄) β ((cardβπ΄) β π΄ β§ π΄ β (cardβπ΄)))) |
7 | 4, 6 | bitr4id 290 |
. . . 4
β’ (π΄ β On β
((cardβπ΄) = π΄ β π΄ β (cardβπ΄))) |
8 | | oncardval 9896 |
. . . . 5
β’ (π΄ β On β
(cardβπ΄) = β© {π¦
β On β£ π¦ β
π΄}) |
9 | 8 | sseq2d 3977 |
. . . 4
β’ (π΄ β On β (π΄ β (cardβπ΄) β π΄ β β© {π¦ β On β£ π¦ β π΄})) |
10 | 7, 9 | bitrd 279 |
. . 3
β’ (π΄ β On β
((cardβπ΄) = π΄ β π΄ β β© {π¦ β On β£ π¦ β π΄})) |
11 | | ssint 4926 |
. . . 4
β’ (π΄ β β© {π¦
β On β£ π¦ β
π΄} β βπ₯ β {π¦ β On β£ π¦ β π΄}π΄ β π₯) |
12 | | breq1 5109 |
. . . . . . . . 9
β’ (π¦ = π₯ β (π¦ β π΄ β π₯ β π΄)) |
13 | 12 | elrab 3646 |
. . . . . . . 8
β’ (π₯ β {π¦ β On β£ π¦ β π΄} β (π₯ β On β§ π₯ β π΄)) |
14 | | ensymb 8945 |
. . . . . . . . 9
β’ (π₯ β π΄ β π΄ β π₯) |
15 | 14 | anbi2i 624 |
. . . . . . . 8
β’ ((π₯ β On β§ π₯ β π΄) β (π₯ β On β§ π΄ β π₯)) |
16 | 13, 15 | bitri 275 |
. . . . . . 7
β’ (π₯ β {π¦ β On β£ π¦ β π΄} β (π₯ β On β§ π΄ β π₯)) |
17 | 16 | imbi1i 350 |
. . . . . 6
β’ ((π₯ β {π¦ β On β£ π¦ β π΄} β π΄ β π₯) β ((π₯ β On β§ π΄ β π₯) β π΄ β π₯)) |
18 | | impexp 452 |
. . . . . 6
β’ (((π₯ β On β§ π΄ β π₯) β π΄ β π₯) β (π₯ β On β (π΄ β π₯ β π΄ β π₯))) |
19 | 17, 18 | bitri 275 |
. . . . 5
β’ ((π₯ β {π¦ β On β£ π¦ β π΄} β π΄ β π₯) β (π₯ β On β (π΄ β π₯ β π΄ β π₯))) |
20 | 19 | ralbii2 3089 |
. . . 4
β’
(βπ₯ β
{π¦ β On β£ π¦ β π΄}π΄ β π₯ β βπ₯ β On (π΄ β π₯ β π΄ β π₯)) |
21 | 11, 20 | bitri 275 |
. . 3
β’ (π΄ β β© {π¦
β On β£ π¦ β
π΄} β βπ₯ β On (π΄ β π₯ β π΄ β π₯)) |
22 | 10, 21 | bitrdi 287 |
. 2
β’ (π΄ β On β
((cardβπ΄) = π΄ β βπ₯ β On (π΄ β π₯ β π΄ β π₯))) |
23 | 3, 22 | biadanii 821 |
1
β’
((cardβπ΄) =
π΄ β (π΄ β On β§ βπ₯ β On (π΄ β π₯ β π΄ β π₯))) |