Step | Hyp | Ref
| Expression |
1 | | cfval 10242 |
. . . 4
β’ (π΄ β On β
(cfβπ΄) = β© {π₯
β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))}) |
2 | 1 | eqeq1d 2735 |
. . 3
β’ (π΄ β On β
((cfβπ΄) = β
β β© {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} = β
)) |
3 | | vex 3479 |
. . . . . . . . 9
β’ π£ β V |
4 | | eqeq1 2737 |
. . . . . . . . . . 11
β’ (π₯ = π£ β (π₯ = (cardβπ¦) β π£ = (cardβπ¦))) |
5 | 4 | anbi1d 631 |
. . . . . . . . . 10
β’ (π₯ = π£ β ((π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)) β (π£ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)))) |
6 | 5 | exbidv 1925 |
. . . . . . . . 9
β’ (π₯ = π£ β (βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)) β βπ¦(π£ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)))) |
7 | 3, 6 | elab 3669 |
. . . . . . . 8
β’ (π£ β {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} β βπ¦(π£ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))) |
8 | | fveq2 6892 |
. . . . . . . . . . . 12
β’ (π£ = (cardβπ¦) β (cardβπ£) =
(cardβ(cardβπ¦))) |
9 | | cardidm 9954 |
. . . . . . . . . . . 12
β’
(cardβ(cardβπ¦)) = (cardβπ¦) |
10 | 8, 9 | eqtrdi 2789 |
. . . . . . . . . . 11
β’ (π£ = (cardβπ¦) β (cardβπ£) = (cardβπ¦)) |
11 | | eqeq2 2745 |
. . . . . . . . . . 11
β’ (π£ = (cardβπ¦) β ((cardβπ£) = π£ β (cardβπ£) = (cardβπ¦))) |
12 | 10, 11 | mpbird 257 |
. . . . . . . . . 10
β’ (π£ = (cardβπ¦) β (cardβπ£) = π£) |
13 | 12 | adantr 482 |
. . . . . . . . 9
β’ ((π£ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)) β (cardβπ£) = π£) |
14 | 13 | exlimiv 1934 |
. . . . . . . 8
β’
(βπ¦(π£ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)) β (cardβπ£) = π£) |
15 | 7, 14 | sylbi 216 |
. . . . . . 7
β’ (π£ β {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} β (cardβπ£) = π£) |
16 | | cardon 9939 |
. . . . . . 7
β’
(cardβπ£)
β On |
17 | 15, 16 | eqeltrrdi 2843 |
. . . . . 6
β’ (π£ β {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} β π£ β On) |
18 | 17 | ssriv 3987 |
. . . . 5
β’ {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} β On |
19 | | onint0 7779 |
. . . . 5
β’ ({π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} β On β (β© {π₯
β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} = β
β β
β {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))})) |
20 | 18, 19 | ax-mp 5 |
. . . 4
β’ (β© {π₯
β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} = β
β β
β {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))}) |
21 | | 0ex 5308 |
. . . . . 6
β’ β
β V |
22 | | eqeq1 2737 |
. . . . . . . 8
β’ (π₯ = β
β (π₯ = (cardβπ¦) β β
=
(cardβπ¦))) |
23 | 22 | anbi1d 631 |
. . . . . . 7
β’ (π₯ = β
β ((π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)) β (β
= (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)))) |
24 | 23 | exbidv 1925 |
. . . . . 6
β’ (π₯ = β
β (βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)) β βπ¦(β
= (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)))) |
25 | 21, 24 | elab 3669 |
. . . . 5
β’ (β
β {π₯ β£
βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} β βπ¦(β
= (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))) |
26 | | onss 7772 |
. . . . . . . . . . 11
β’ (π΄ β On β π΄ β On) |
27 | | sstr 3991 |
. . . . . . . . . . . 12
β’ ((π¦ β π΄ β§ π΄ β On) β π¦ β On) |
28 | 27 | ancoms 460 |
. . . . . . . . . . 11
β’ ((π΄ β On β§ π¦ β π΄) β π¦ β On) |
29 | 26, 28 | sylan 581 |
. . . . . . . . . 10
β’ ((π΄ β On β§ π¦ β π΄) β π¦ β On) |
30 | 29 | 3adant2 1132 |
. . . . . . . . 9
β’ ((π΄ β On β§ β
=
(cardβπ¦) β§ π¦ β π΄) β π¦ β On) |
31 | 30 | 3adant3r 1182 |
. . . . . . . 8
β’ ((π΄ β On β§ β
=
(cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)) β π¦ β On) |
32 | | simp2 1138 |
. . . . . . . 8
β’ ((π΄ β On β§ β
=
(cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)) β β
= (cardβπ¦)) |
33 | | simp3 1139 |
. . . . . . . 8
β’ ((π΄ β On β§ β
=
(cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)) β (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)) |
34 | | eqcom 2740 |
. . . . . . . . . . . 12
β’ (β
= (cardβπ¦) β
(cardβπ¦) =
β
) |
35 | | vex 3479 |
. . . . . . . . . . . . . 14
β’ π¦ β V |
36 | | onssnum 10035 |
. . . . . . . . . . . . . 14
β’ ((π¦ β V β§ π¦ β On) β π¦ β dom
card) |
37 | 35, 36 | mpan 689 |
. . . . . . . . . . . . 13
β’ (π¦ β On β π¦ β dom
card) |
38 | | cardnueq0 9959 |
. . . . . . . . . . . . 13
β’ (π¦ β dom card β
((cardβπ¦) = β
β π¦ =
β
)) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . 12
β’ (π¦ β On β
((cardβπ¦) = β
β π¦ =
β
)) |
40 | 34, 39 | bitrid 283 |
. . . . . . . . . . 11
β’ (π¦ β On β (β
=
(cardβπ¦) β π¦ = β
)) |
41 | 40 | biimpa 478 |
. . . . . . . . . 10
β’ ((π¦ β On β§ β
=
(cardβπ¦)) β
π¦ =
β
) |
42 | | sseq1 4008 |
. . . . . . . . . . . 12
β’ (π¦ = β
β (π¦ β π΄ β β
β π΄)) |
43 | | rexeq 3322 |
. . . . . . . . . . . . 13
β’ (π¦ = β
β (βπ€ β π¦ π§ β π€ β βπ€ β β
π§ β π€)) |
44 | 43 | ralbidv 3178 |
. . . . . . . . . . . 12
β’ (π¦ = β
β (βπ§ β π΄ βπ€ β π¦ π§ β π€ β βπ§ β π΄ βπ€ β β
π§ β π€)) |
45 | 42, 44 | anbi12d 632 |
. . . . . . . . . . 11
β’ (π¦ = β
β ((π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€) β (β
β π΄ β§ βπ§ β π΄ βπ€ β β
π§ β π€))) |
46 | 45 | biimpa 478 |
. . . . . . . . . 10
β’ ((π¦ = β
β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)) β (β
β π΄ β§ βπ§ β π΄ βπ€ β β
π§ β π€)) |
47 | 41, 46 | sylan 581 |
. . . . . . . . 9
β’ (((π¦ β On β§ β
=
(cardβπ¦)) β§
(π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)) β (β
β π΄ β§ βπ§ β π΄ βπ€ β β
π§ β π€)) |
48 | | rex0 4358 |
. . . . . . . . . . . . 13
β’ Β¬
βπ€ β β
π§ β π€ |
49 | 48 | rgenw 3066 |
. . . . . . . . . . . 12
β’
βπ§ β
π΄ Β¬ βπ€ β β
π§ β π€ |
50 | | r19.2z 4495 |
. . . . . . . . . . . 12
β’ ((π΄ β β
β§
βπ§ β π΄ Β¬ βπ€ β β
π§ β π€) β βπ§ β π΄ Β¬ βπ€ β β
π§ β π€) |
51 | 49, 50 | mpan2 690 |
. . . . . . . . . . 11
β’ (π΄ β β
β
βπ§ β π΄ Β¬ βπ€ β β
π§ β π€) |
52 | | rexnal 3101 |
. . . . . . . . . . 11
β’
(βπ§ β
π΄ Β¬ βπ€ β β
π§ β π€ β Β¬ βπ§ β π΄ βπ€ β β
π§ β π€) |
53 | 51, 52 | sylib 217 |
. . . . . . . . . 10
β’ (π΄ β β
β Β¬
βπ§ β π΄ βπ€ β β
π§ β π€) |
54 | 53 | necon4ai 2973 |
. . . . . . . . 9
β’
(βπ§ β
π΄ βπ€ β β
π§ β π€ β π΄ = β
) |
55 | 47, 54 | simpl2im 505 |
. . . . . . . 8
β’ (((π¦ β On β§ β
=
(cardβπ¦)) β§
(π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)) β π΄ = β
) |
56 | 31, 32, 33, 55 | syl21anc 837 |
. . . . . . 7
β’ ((π΄ β On β§ β
=
(cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)) β π΄ = β
) |
57 | 56 | 3expib 1123 |
. . . . . 6
β’ (π΄ β On β ((β
=
(cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)) β π΄ = β
)) |
58 | 57 | exlimdv 1937 |
. . . . 5
β’ (π΄ β On β (βπ¦(β
= (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)) β π΄ = β
)) |
59 | 25, 58 | biimtrid 241 |
. . . 4
β’ (π΄ β On β (β
β {π₯ β£
βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} β π΄ = β
)) |
60 | 20, 59 | biimtrid 241 |
. . 3
β’ (π΄ β On β (β© {π₯
β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} = β
β π΄ = β
)) |
61 | 2, 60 | sylbid 239 |
. 2
β’ (π΄ β On β
((cfβπ΄) = β
β π΄ =
β
)) |
62 | | fveq2 6892 |
. . 3
β’ (π΄ = β
β
(cfβπ΄) =
(cfββ
)) |
63 | | cf0 10246 |
. . 3
β’
(cfββ
) = β
|
64 | 62, 63 | eqtrdi 2789 |
. 2
β’ (π΄ = β
β
(cfβπ΄) =
β
) |
65 | 61, 64 | impbid1 224 |
1
β’ (π΄ β On β
((cfβπ΄) = β
β π΄ =
β
)) |