Step | Hyp | Ref
| Expression |
1 | | cfval 10183 |
. . . 4
β’ (π΄ β On β
(cfβπ΄) = β© {π₯
β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))}) |
2 | | vex 3449 |
. . . . . . . . 9
β’ π£ β V |
3 | | eqeq1 2740 |
. . . . . . . . . . 11
β’ (π₯ = π£ β (π₯ = (cardβπ¦) β π£ = (cardβπ¦))) |
4 | 3 | anbi1d 630 |
. . . . . . . . . 10
β’ (π₯ = π£ β ((π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)) β (π£ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)))) |
5 | 4 | exbidv 1924 |
. . . . . . . . 9
β’ (π₯ = π£ β (βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)) β βπ¦(π£ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)))) |
6 | 2, 5 | elab 3630 |
. . . . . . . 8
β’ (π£ β {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} β βπ¦(π£ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))) |
7 | | fveq2 6842 |
. . . . . . . . . . . 12
β’ (π£ = (cardβπ¦) β (cardβπ£) =
(cardβ(cardβπ¦))) |
8 | | cardidm 9895 |
. . . . . . . . . . . 12
β’
(cardβ(cardβπ¦)) = (cardβπ¦) |
9 | 7, 8 | eqtrdi 2792 |
. . . . . . . . . . 11
β’ (π£ = (cardβπ¦) β (cardβπ£) = (cardβπ¦)) |
10 | | eqeq2 2748 |
. . . . . . . . . . 11
β’ (π£ = (cardβπ¦) β ((cardβπ£) = π£ β (cardβπ£) = (cardβπ¦))) |
11 | 9, 10 | mpbird 256 |
. . . . . . . . . 10
β’ (π£ = (cardβπ¦) β (cardβπ£) = π£) |
12 | 11 | adantr 481 |
. . . . . . . . 9
β’ ((π£ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)) β (cardβπ£) = π£) |
13 | 12 | exlimiv 1933 |
. . . . . . . 8
β’
(βπ¦(π£ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)) β (cardβπ£) = π£) |
14 | 6, 13 | sylbi 216 |
. . . . . . 7
β’ (π£ β {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} β (cardβπ£) = π£) |
15 | | cardon 9880 |
. . . . . . 7
β’
(cardβπ£)
β On |
16 | 14, 15 | eqeltrrdi 2846 |
. . . . . 6
β’ (π£ β {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} β π£ β On) |
17 | 16 | ssriv 3948 |
. . . . 5
β’ {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} β On |
18 | | fvex 6855 |
. . . . . . 7
β’
(cfβπ΄) β
V |
19 | 1, 18 | eqeltrrdi 2846 |
. . . . . 6
β’ (π΄ β On β β© {π₯
β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} β V) |
20 | | intex 5294 |
. . . . . 6
β’ ({π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} β β
β β© {π₯
β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} β V) |
21 | 19, 20 | sylibr 233 |
. . . . 5
β’ (π΄ β On β {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} β β
) |
22 | | onint 7725 |
. . . . 5
β’ (({π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} β On β§ {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} β β
) β β© {π₯
β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} β {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))}) |
23 | 17, 21, 22 | sylancr 587 |
. . . 4
β’ (π΄ β On β β© {π₯
β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} β {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))}) |
24 | 1, 23 | eqeltrd 2837 |
. . 3
β’ (π΄ β On β
(cfβπ΄) β {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))}) |
25 | | fveq2 6842 |
. . . . 5
β’ (π£ = (cfβπ΄) β (cardβπ£) = (cardβ(cfβπ΄))) |
26 | | id 22 |
. . . . 5
β’ (π£ = (cfβπ΄) β π£ = (cfβπ΄)) |
27 | 25, 26 | eqeq12d 2752 |
. . . 4
β’ (π£ = (cfβπ΄) β ((cardβπ£) = π£ β (cardβ(cfβπ΄)) = (cfβπ΄))) |
28 | 27, 14 | vtoclga 3534 |
. . 3
β’
((cfβπ΄) β
{π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} β (cardβ(cfβπ΄)) = (cfβπ΄)) |
29 | 24, 28 | syl 17 |
. 2
β’ (π΄ β On β
(cardβ(cfβπ΄)) =
(cfβπ΄)) |
30 | | cff 10184 |
. . . . . 6
β’
cf:OnβΆOn |
31 | 30 | fdmi 6680 |
. . . . 5
β’ dom cf =
On |
32 | 31 | eleq2i 2829 |
. . . 4
β’ (π΄ β dom cf β π΄ β On) |
33 | | ndmfv 6877 |
. . . 4
β’ (Β¬
π΄ β dom cf β
(cfβπ΄) =
β
) |
34 | 32, 33 | sylnbir 330 |
. . 3
β’ (Β¬
π΄ β On β
(cfβπ΄) =
β
) |
35 | | card0 9894 |
. . . 4
β’
(cardββ
) = β
|
36 | | fveq2 6842 |
. . . 4
β’
((cfβπ΄) =
β
β (cardβ(cfβπ΄)) = (cardββ
)) |
37 | | id 22 |
. . . 4
β’
((cfβπ΄) =
β
β (cfβπ΄)
= β
) |
38 | 35, 36, 37 | 3eqtr4a 2802 |
. . 3
β’
((cfβπ΄) =
β
β (cardβ(cfβπ΄)) = (cfβπ΄)) |
39 | 34, 38 | syl 17 |
. 2
β’ (Β¬
π΄ β On β
(cardβ(cfβπ΄)) =
(cfβπ΄)) |
40 | 29, 39 | pm2.61i 182 |
1
β’
(cardβ(cfβπ΄)) = (cfβπ΄) |