Step | Hyp | Ref
| Expression |
1 | | cardprclem.1 |
. . . . . . . . 9
β’ π΄ = {π₯ β£ (cardβπ₯) = π₯} |
2 | 1 | eleq2i 2826 |
. . . . . . . 8
β’ (π₯ β π΄ β π₯ β {π₯ β£ (cardβπ₯) = π₯}) |
3 | | abid 2714 |
. . . . . . . 8
β’ (π₯ β {π₯ β£ (cardβπ₯) = π₯} β (cardβπ₯) = π₯) |
4 | | iscard 9916 |
. . . . . . . 8
β’
((cardβπ₯) =
π₯ β (π₯ β On β§ βπ¦ β π₯ π¦ βΊ π₯)) |
5 | 2, 3, 4 | 3bitri 297 |
. . . . . . 7
β’ (π₯ β π΄ β (π₯ β On β§ βπ¦ β π₯ π¦ βΊ π₯)) |
6 | 5 | simplbi 499 |
. . . . . 6
β’ (π₯ β π΄ β π₯ β On) |
7 | 6 | ssriv 3949 |
. . . . 5
β’ π΄ β On |
8 | | ssonuni 7715 |
. . . . 5
β’ (π΄ β V β (π΄ β On β βͺ π΄
β On)) |
9 | 7, 8 | mpi 20 |
. . . 4
β’ (π΄ β V β βͺ π΄
β On) |
10 | | domrefg 8930 |
. . . . 5
β’ (βͺ π΄
β On β βͺ π΄ βΌ βͺ π΄) |
11 | 9, 10 | syl 17 |
. . . 4
β’ (π΄ β V β βͺ π΄
βΌ βͺ π΄) |
12 | | elharval 9502 |
. . . 4
β’ (βͺ π΄
β (harββͺ π΄) β (βͺ π΄ β On β§ βͺ π΄
βΌ βͺ π΄)) |
13 | 9, 11, 12 | sylanbrc 584 |
. . 3
β’ (π΄ β V β βͺ π΄
β (harββͺ π΄)) |
14 | 7 | sseli 3941 |
. . . . . . . 8
β’ (π§ β π΄ β π§ β On) |
15 | | domrefg 8930 |
. . . . . . . . . 10
β’ (π§ β On β π§ βΌ π§) |
16 | 15 | ancli 550 |
. . . . . . . . 9
β’ (π§ β On β (π§ β On β§ π§ βΌ π§)) |
17 | | elharval 9502 |
. . . . . . . . 9
β’ (π§ β (harβπ§) β (π§ β On β§ π§ βΌ π§)) |
18 | 16, 17 | sylibr 233 |
. . . . . . . 8
β’ (π§ β On β π§ β (harβπ§)) |
19 | 14, 18 | syl 17 |
. . . . . . 7
β’ (π§ β π΄ β π§ β (harβπ§)) |
20 | | harcard 9919 |
. . . . . . . 8
β’
(cardβ(harβπ§)) = (harβπ§) |
21 | | fvex 6856 |
. . . . . . . . 9
β’
(harβπ§) β
V |
22 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π₯ = (harβπ§) β (cardβπ₯) = (cardβ(harβπ§))) |
23 | | id 22 |
. . . . . . . . . 10
β’ (π₯ = (harβπ§) β π₯ = (harβπ§)) |
24 | 22, 23 | eqeq12d 2749 |
. . . . . . . . 9
β’ (π₯ = (harβπ§) β ((cardβπ₯) = π₯ β (cardβ(harβπ§)) = (harβπ§))) |
25 | 21, 24, 1 | elab2 3635 |
. . . . . . . 8
β’
((harβπ§)
β π΄ β
(cardβ(harβπ§))
= (harβπ§)) |
26 | 20, 25 | mpbir 230 |
. . . . . . 7
β’
(harβπ§) β
π΄ |
27 | | eleq2 2823 |
. . . . . . . . 9
β’ (π€ = (harβπ§) β (π§ β π€ β π§ β (harβπ§))) |
28 | | eleq1 2822 |
. . . . . . . . 9
β’ (π€ = (harβπ§) β (π€ β π΄ β (harβπ§) β π΄)) |
29 | 27, 28 | anbi12d 632 |
. . . . . . . 8
β’ (π€ = (harβπ§) β ((π§ β π€ β§ π€ β π΄) β (π§ β (harβπ§) β§ (harβπ§) β π΄))) |
30 | 21, 29 | spcev 3564 |
. . . . . . 7
β’ ((π§ β (harβπ§) β§ (harβπ§) β π΄) β βπ€(π§ β π€ β§ π€ β π΄)) |
31 | 19, 26, 30 | sylancl 587 |
. . . . . 6
β’ (π§ β π΄ β βπ€(π§ β π€ β§ π€ β π΄)) |
32 | | eluni 4869 |
. . . . . 6
β’ (π§ β βͺ π΄
β βπ€(π§ β π€ β§ π€ β π΄)) |
33 | 31, 32 | sylibr 233 |
. . . . 5
β’ (π§ β π΄ β π§ β βͺ π΄) |
34 | 33 | ssriv 3949 |
. . . 4
β’ π΄ β βͺ π΄ |
35 | | harcard 9919 |
. . . . 5
β’
(cardβ(harββͺ π΄)) = (harββͺ
π΄) |
36 | | fvex 6856 |
. . . . . 6
β’
(harββͺ π΄) β V |
37 | | fveq2 6843 |
. . . . . . 7
β’ (π₯ = (harββͺ π΄)
β (cardβπ₯) =
(cardβ(harββͺ π΄))) |
38 | | id 22 |
. . . . . . 7
β’ (π₯ = (harββͺ π΄)
β π₯ = (harββͺ π΄)) |
39 | 37, 38 | eqeq12d 2749 |
. . . . . 6
β’ (π₯ = (harββͺ π΄)
β ((cardβπ₯) =
π₯ β
(cardβ(harββͺ π΄)) = (harββͺ
π΄))) |
40 | 36, 39, 1 | elab2 3635 |
. . . . 5
β’
((harββͺ π΄) β π΄ β (cardβ(harββͺ π΄))
= (harββͺ π΄)) |
41 | 35, 40 | mpbir 230 |
. . . 4
β’
(harββͺ π΄) β π΄ |
42 | 34, 41 | sselii 3942 |
. . 3
β’
(harββͺ π΄) β βͺ π΄ |
43 | 13, 42 | jctir 522 |
. 2
β’ (π΄ β V β (βͺ π΄
β (harββͺ π΄) β§ (harββͺ π΄)
β βͺ π΄)) |
44 | | eloni 6328 |
. . 3
β’ (βͺ π΄
β On β Ord βͺ π΄) |
45 | | ordn2lp 6338 |
. . 3
β’ (Ord
βͺ π΄ β Β¬ (βͺ
π΄ β (harββͺ π΄)
β§ (harββͺ π΄) β βͺ π΄)) |
46 | 9, 44, 45 | 3syl 18 |
. 2
β’ (π΄ β V β Β¬ (βͺ π΄
β (harββͺ π΄) β§ (harββͺ π΄)
β βͺ π΄)) |
47 | 43, 46 | pm2.65i 193 |
1
β’ Β¬
π΄ β V |