Step | Hyp | Ref
| Expression |
1 | | df-cf 9940 |
. 2
β’ cf =
(π₯ β On β¦ β© {π¦
β£ βπ§(π¦ = (cardβπ§) β§ (π§ β π₯ β§ βπ€ β π₯ βπ£ β π§ π€ β π£))}) |
2 | | cardon 9943 |
. . . . . . 7
β’
(cardβπ§)
β On |
3 | | eleq1 2820 |
. . . . . . 7
β’ (π¦ = (cardβπ§) β (π¦ β On β (cardβπ§) β On)) |
4 | 2, 3 | mpbiri 258 |
. . . . . 6
β’ (π¦ = (cardβπ§) β π¦ β On) |
5 | 4 | adantr 480 |
. . . . 5
β’ ((π¦ = (cardβπ§) β§ (π§ β π₯ β§ βπ€ β π₯ βπ£ β π§ π€ β π£)) β π¦ β On) |
6 | 5 | exlimiv 1932 |
. . . 4
β’
(βπ§(π¦ = (cardβπ§) β§ (π§ β π₯ β§ βπ€ β π₯ βπ£ β π§ π€ β π£)) β π¦ β On) |
7 | 6 | abssi 4067 |
. . 3
β’ {π¦ β£ βπ§(π¦ = (cardβπ§) β§ (π§ β π₯ β§ βπ€ β π₯ βπ£ β π§ π€ β π£))} β On |
8 | | cflem 10245 |
. . . 4
β’ (π₯ β On β βπ¦βπ§(π¦ = (cardβπ§) β§ (π§ β π₯ β§ βπ€ β π₯ βπ£ β π§ π€ β π£))) |
9 | | abn0 4380 |
. . . 4
β’ ({π¦ β£ βπ§(π¦ = (cardβπ§) β§ (π§ β π₯ β§ βπ€ β π₯ βπ£ β π§ π€ β π£))} β β
β βπ¦βπ§(π¦ = (cardβπ§) β§ (π§ β π₯ β§ βπ€ β π₯ βπ£ β π§ π€ β π£))) |
10 | 8, 9 | sylibr 233 |
. . 3
β’ (π₯ β On β {π¦ β£ βπ§(π¦ = (cardβπ§) β§ (π§ β π₯ β§ βπ€ β π₯ βπ£ β π§ π€ β π£))} β β
) |
11 | | oninton 7787 |
. . 3
β’ (({π¦ β£ βπ§(π¦ = (cardβπ§) β§ (π§ β π₯ β§ βπ€ β π₯ βπ£ β π§ π€ β π£))} β On β§ {π¦ β£ βπ§(π¦ = (cardβπ§) β§ (π§ β π₯ β§ βπ€ β π₯ βπ£ β π§ π€ β π£))} β β
) β β© {π¦
β£ βπ§(π¦ = (cardβπ§) β§ (π§ β π₯ β§ βπ€ β π₯ βπ£ β π§ π€ β π£))} β On) |
12 | 7, 10, 11 | sylancr 586 |
. 2
β’ (π₯ β On β β© {π¦
β£ βπ§(π¦ = (cardβπ§) β§ (π§ β π₯ β§ βπ€ β π₯ βπ£ β π§ π€ β π£))} β On) |
13 | 1, 12 | fmpti 7113 |
1
β’
cf:OnβΆOn |