Step | Hyp | Ref
| Expression |
1 | | cfval 10191 |
. . 3
β’ (π΄ β On β
(cfβπ΄) = β© {π₯
β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))}) |
2 | | df-sn 4591 |
. . . . . 6
β’
{(cardβπ΄)} =
{π₯ β£ π₯ = (cardβπ΄)} |
3 | | ssid 3970 |
. . . . . . . . 9
β’ π΄ β π΄ |
4 | | ssid 3970 |
. . . . . . . . . . 11
β’ π§ β π§ |
5 | | sseq2 3974 |
. . . . . . . . . . . 12
β’ (π€ = π§ β (π§ β π€ β π§ β π§)) |
6 | 5 | rspcev 3583 |
. . . . . . . . . . 11
β’ ((π§ β π΄ β§ π§ β π§) β βπ€ β π΄ π§ β π€) |
7 | 4, 6 | mpan2 690 |
. . . . . . . . . 10
β’ (π§ β π΄ β βπ€ β π΄ π§ β π€) |
8 | 7 | rgen 3063 |
. . . . . . . . 9
β’
βπ§ β
π΄ βπ€ β π΄ π§ β π€ |
9 | 3, 8 | pm3.2i 472 |
. . . . . . . 8
β’ (π΄ β π΄ β§ βπ§ β π΄ βπ€ β π΄ π§ β π€) |
10 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π¦ = π΄ β (cardβπ¦) = (cardβπ΄)) |
11 | 10 | eqeq2d 2744 |
. . . . . . . . . 10
β’ (π¦ = π΄ β (π₯ = (cardβπ¦) β π₯ = (cardβπ΄))) |
12 | | sseq1 3973 |
. . . . . . . . . . 11
β’ (π¦ = π΄ β (π¦ β π΄ β π΄ β π΄)) |
13 | | rexeq 3309 |
. . . . . . . . . . . 12
β’ (π¦ = π΄ β (βπ€ β π¦ π§ β π€ β βπ€ β π΄ π§ β π€)) |
14 | 13 | ralbidv 3171 |
. . . . . . . . . . 11
β’ (π¦ = π΄ β (βπ§ β π΄ βπ€ β π¦ π§ β π€ β βπ§ β π΄ βπ€ β π΄ π§ β π€)) |
15 | 12, 14 | anbi12d 632 |
. . . . . . . . . 10
β’ (π¦ = π΄ β ((π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€) β (π΄ β π΄ β§ βπ§ β π΄ βπ€ β π΄ π§ β π€))) |
16 | 11, 15 | anbi12d 632 |
. . . . . . . . 9
β’ (π¦ = π΄ β ((π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)) β (π₯ = (cardβπ΄) β§ (π΄ β π΄ β§ βπ§ β π΄ βπ€ β π΄ π§ β π€)))) |
17 | 16 | spcegv 3558 |
. . . . . . . 8
β’ (π΄ β On β ((π₯ = (cardβπ΄) β§ (π΄ β π΄ β§ βπ§ β π΄ βπ€ β π΄ π§ β π€)) β βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)))) |
18 | 9, 17 | mpan2i 696 |
. . . . . . 7
β’ (π΄ β On β (π₯ = (cardβπ΄) β βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)))) |
19 | 18 | ss2abdv 4024 |
. . . . . 6
β’ (π΄ β On β {π₯ β£ π₯ = (cardβπ΄)} β {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))}) |
20 | 2, 19 | eqsstrid 3996 |
. . . . 5
β’ (π΄ β On β
{(cardβπ΄)} β
{π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))}) |
21 | | intss 4934 |
. . . . 5
β’
({(cardβπ΄)}
β {π₯ β£
βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} β β©
{π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} β β©
{(cardβπ΄)}) |
22 | 20, 21 | syl 17 |
. . . 4
β’ (π΄ β On β β© {π₯
β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} β β©
{(cardβπ΄)}) |
23 | | fvex 6859 |
. . . . 5
β’
(cardβπ΄)
β V |
24 | 23 | intsn 4951 |
. . . 4
β’ β© {(cardβπ΄)} = (cardβπ΄) |
25 | 22, 24 | sseqtrdi 3998 |
. . 3
β’ (π΄ β On β β© {π₯
β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} β (cardβπ΄)) |
26 | 1, 25 | eqsstrd 3986 |
. 2
β’ (π΄ β On β
(cfβπ΄) β
(cardβπ΄)) |
27 | | cff 10192 |
. . . . . 6
β’
cf:OnβΆOn |
28 | 27 | fdmi 6684 |
. . . . 5
β’ dom cf =
On |
29 | 28 | eleq2i 2826 |
. . . 4
β’ (π΄ β dom cf β π΄ β On) |
30 | | ndmfv 6881 |
. . . 4
β’ (Β¬
π΄ β dom cf β
(cfβπ΄) =
β
) |
31 | 29, 30 | sylnbir 331 |
. . 3
β’ (Β¬
π΄ β On β
(cfβπ΄) =
β
) |
32 | | 0ss 4360 |
. . 3
β’ β
β (cardβπ΄) |
33 | 31, 32 | eqsstrdi 4002 |
. 2
β’ (Β¬
π΄ β On β
(cfβπ΄) β
(cardβπ΄)) |
34 | 26, 33 | pm2.61i 182 |
1
β’
(cfβπ΄) β
(cardβπ΄) |