Step | Hyp | Ref
| Expression |
1 | | onintrab2 7733 |
. . . 4
β’
(βπ₯ β On
π΄ βΊ π₯ β β© {π₯
β On β£ π΄ βΊ
π₯} β
On) |
2 | 1 | biimpi 215 |
. . 3
β’
(βπ₯ β On
π΄ βΊ π₯ β β© {π₯
β On β£ π΄ βΊ
π₯} β
On) |
3 | 2 | adantr 482 |
. . . . . 6
β’
((βπ₯ β On
π΄ βΊ π₯ β§ π¦ β β© {π₯ β On β£ π΄ βΊ π₯}) β β© {π₯ β On β£ π΄ βΊ π₯} β On) |
4 | | eloni 6328 |
. . . . . . . 8
β’ (β© {π₯
β On β£ π΄ βΊ
π₯} β On β Ord
β© {π₯ β On β£ π΄ βΊ π₯}) |
5 | | ordelss 6334 |
. . . . . . . 8
β’ ((Ord
β© {π₯ β On β£ π΄ βΊ π₯} β§ π¦ β β© {π₯ β On β£ π΄ βΊ π₯}) β π¦ β β© {π₯ β On β£ π΄ βΊ π₯}) |
6 | 4, 5 | sylan 581 |
. . . . . . 7
β’ ((β© {π₯
β On β£ π΄ βΊ
π₯} β On β§ π¦ β β© {π₯
β On β£ π΄ βΊ
π₯}) β π¦ β β© {π₯
β On β£ π΄ βΊ
π₯}) |
7 | 1, 6 | sylanb 582 |
. . . . . 6
β’
((βπ₯ β On
π΄ βΊ π₯ β§ π¦ β β© {π₯ β On β£ π΄ βΊ π₯}) β π¦ β β© {π₯ β On β£ π΄ βΊ π₯}) |
8 | | ssdomg 8943 |
. . . . . 6
β’ (β© {π₯
β On β£ π΄ βΊ
π₯} β On β (π¦ β β© {π₯
β On β£ π΄ βΊ
π₯} β π¦ βΌ β© {π₯
β On β£ π΄ βΊ
π₯})) |
9 | 3, 7, 8 | sylc 65 |
. . . . 5
β’
((βπ₯ β On
π΄ βΊ π₯ β§ π¦ β β© {π₯ β On β£ π΄ βΊ π₯}) β π¦ βΌ β© {π₯ β On β£ π΄ βΊ π₯}) |
10 | | onelon 6343 |
. . . . . . . 8
β’ ((β© {π₯
β On β£ π΄ βΊ
π₯} β On β§ π¦ β β© {π₯
β On β£ π΄ βΊ
π₯}) β π¦ β On) |
11 | 1, 10 | sylanb 582 |
. . . . . . 7
β’
((βπ₯ β On
π΄ βΊ π₯ β§ π¦ β β© {π₯ β On β£ π΄ βΊ π₯}) β π¦ β On) |
12 | | nfcv 2904 |
. . . . . . . . . . . . . 14
β’
β²π₯π΄ |
13 | | nfcv 2904 |
. . . . . . . . . . . . . 14
β’
β²π₯
βΊ |
14 | | nfrab1 3425 |
. . . . . . . . . . . . . . 15
β’
β²π₯{π₯ β On β£ π΄ βΊ π₯} |
15 | 14 | nfint 4918 |
. . . . . . . . . . . . . 14
β’
β²π₯β© {π₯
β On β£ π΄ βΊ
π₯} |
16 | 12, 13, 15 | nfbr 5153 |
. . . . . . . . . . . . 13
β’
β²π₯ π΄ βΊ β© {π₯
β On β£ π΄ βΊ
π₯} |
17 | | breq2 5110 |
. . . . . . . . . . . . 13
β’ (π₯ = β©
{π₯ β On β£ π΄ βΊ π₯} β (π΄ βΊ π₯ β π΄ βΊ β© {π₯ β On β£ π΄ βΊ π₯})) |
18 | 16, 17 | onminsb 7730 |
. . . . . . . . . . . 12
β’
(βπ₯ β On
π΄ βΊ π₯ β π΄ βΊ β© {π₯ β On β£ π΄ βΊ π₯}) |
19 | | sdomentr 9058 |
. . . . . . . . . . . 12
β’ ((π΄ βΊ β© {π₯
β On β£ π΄ βΊ
π₯} β§ β© {π₯
β On β£ π΄ βΊ
π₯} β π¦) β π΄ βΊ π¦) |
20 | 18, 19 | sylan 581 |
. . . . . . . . . . 11
β’
((βπ₯ β On
π΄ βΊ π₯ β§ β© {π₯
β On β£ π΄ βΊ
π₯} β π¦) β π΄ βΊ π¦) |
21 | | breq2 5110 |
. . . . . . . . . . . . . 14
β’ (π₯ = π¦ β (π΄ βΊ π₯ β π΄ βΊ π¦)) |
22 | 21 | elrab 3646 |
. . . . . . . . . . . . 13
β’ (π¦ β {π₯ β On β£ π΄ βΊ π₯} β (π¦ β On β§ π΄ βΊ π¦)) |
23 | | ssrab2 4038 |
. . . . . . . . . . . . . 14
β’ {π₯ β On β£ π΄ βΊ π₯} β On |
24 | | onnmin 7734 |
. . . . . . . . . . . . . 14
β’ (({π₯ β On β£ π΄ βΊ π₯} β On β§ π¦ β {π₯ β On β£ π΄ βΊ π₯}) β Β¬ π¦ β β© {π₯ β On β£ π΄ βΊ π₯}) |
25 | 23, 24 | mpan 689 |
. . . . . . . . . . . . 13
β’ (π¦ β {π₯ β On β£ π΄ βΊ π₯} β Β¬ π¦ β β© {π₯ β On β£ π΄ βΊ π₯}) |
26 | 22, 25 | sylbir 234 |
. . . . . . . . . . . 12
β’ ((π¦ β On β§ π΄ βΊ π¦) β Β¬ π¦ β β© {π₯ β On β£ π΄ βΊ π₯}) |
27 | 26 | expcom 415 |
. . . . . . . . . . 11
β’ (π΄ βΊ π¦ β (π¦ β On β Β¬ π¦ β β© {π₯ β On β£ π΄ βΊ π₯})) |
28 | 20, 27 | syl 17 |
. . . . . . . . . 10
β’
((βπ₯ β On
π΄ βΊ π₯ β§ β© {π₯
β On β£ π΄ βΊ
π₯} β π¦) β (π¦ β On β Β¬ π¦ β β© {π₯ β On β£ π΄ βΊ π₯})) |
29 | 28 | impancom 453 |
. . . . . . . . 9
β’
((βπ₯ β On
π΄ βΊ π₯ β§ π¦ β On) β (β© {π₯
β On β£ π΄ βΊ
π₯} β π¦ β Β¬ π¦ β β© {π₯ β On β£ π΄ βΊ π₯})) |
30 | 29 | con2d 134 |
. . . . . . . 8
β’
((βπ₯ β On
π΄ βΊ π₯ β§ π¦ β On) β (π¦ β β© {π₯ β On β£ π΄ βΊ π₯} β Β¬ β©
{π₯ β On β£ π΄ βΊ π₯} β π¦)) |
31 | 30 | impancom 453 |
. . . . . . 7
β’
((βπ₯ β On
π΄ βΊ π₯ β§ π¦ β β© {π₯ β On β£ π΄ βΊ π₯}) β (π¦ β On β Β¬ β© {π₯
β On β£ π΄ βΊ
π₯} β π¦)) |
32 | 11, 31 | mpd 15 |
. . . . . 6
β’
((βπ₯ β On
π΄ βΊ π₯ β§ π¦ β β© {π₯ β On β£ π΄ βΊ π₯}) β Β¬ β©
{π₯ β On β£ π΄ βΊ π₯} β π¦) |
33 | | ensym 8946 |
. . . . . 6
β’ (π¦ β β© {π₯
β On β£ π΄ βΊ
π₯} β β© {π₯
β On β£ π΄ βΊ
π₯} β π¦) |
34 | 32, 33 | nsyl 140 |
. . . . 5
β’
((βπ₯ β On
π΄ βΊ π₯ β§ π¦ β β© {π₯ β On β£ π΄ βΊ π₯}) β Β¬ π¦ β β© {π₯ β On β£ π΄ βΊ π₯}) |
35 | | brsdom 8918 |
. . . . 5
β’ (π¦ βΊ β© {π₯
β On β£ π΄ βΊ
π₯} β (π¦ βΌ β© {π₯
β On β£ π΄ βΊ
π₯} β§ Β¬ π¦ β β© {π₯
β On β£ π΄ βΊ
π₯})) |
36 | 9, 34, 35 | sylanbrc 584 |
. . . 4
β’
((βπ₯ β On
π΄ βΊ π₯ β§ π¦ β β© {π₯ β On β£ π΄ βΊ π₯}) β π¦ βΊ β© {π₯ β On β£ π΄ βΊ π₯}) |
37 | 36 | ralrimiva 3140 |
. . 3
β’
(βπ₯ β On
π΄ βΊ π₯ β βπ¦ β β© {π₯
β On β£ π΄ βΊ
π₯}π¦ βΊ β© {π₯ β On β£ π΄ βΊ π₯}) |
38 | | iscard 9916 |
. . 3
β’
((cardββ© {π₯ β On β£ π΄ βΊ π₯}) = β© {π₯ β On β£ π΄ βΊ π₯} β (β© {π₯ β On β£ π΄ βΊ π₯} β On β§ βπ¦ β β© {π₯ β On β£ π΄ βΊ π₯}π¦ βΊ β© {π₯ β On β£ π΄ βΊ π₯})) |
39 | 2, 37, 38 | sylanbrc 584 |
. 2
β’
(βπ₯ β On
π΄ βΊ π₯ β (cardββ© {π₯
β On β£ π΄ βΊ
π₯}) = β© {π₯
β On β£ π΄ βΊ
π₯}) |
40 | | vprc 5273 |
. . . . . 6
β’ Β¬ V
β V |
41 | | inteq 4911 |
. . . . . . . 8
β’ ({π₯ β On β£ π΄ βΊ π₯} = β
β β© {π₯
β On β£ π΄ βΊ
π₯} = β© β
) |
42 | | int0 4924 |
. . . . . . . 8
β’ β© β
= V |
43 | 41, 42 | eqtrdi 2789 |
. . . . . . 7
β’ ({π₯ β On β£ π΄ βΊ π₯} = β
β β© {π₯
β On β£ π΄ βΊ
π₯} = V) |
44 | 43 | eleq1d 2819 |
. . . . . 6
β’ ({π₯ β On β£ π΄ βΊ π₯} = β
β (β© {π₯
β On β£ π΄ βΊ
π₯} β V β V β
V)) |
45 | 40, 44 | mtbiri 327 |
. . . . 5
β’ ({π₯ β On β£ π΄ βΊ π₯} = β
β Β¬ β© {π₯
β On β£ π΄ βΊ
π₯} β
V) |
46 | | fvex 6856 |
. . . . . 6
β’
(cardββ© {π₯ β On β£ π΄ βΊ π₯}) β V |
47 | | eleq1 2822 |
. . . . . 6
β’
((cardββ© {π₯ β On β£ π΄ βΊ π₯}) = β© {π₯ β On β£ π΄ βΊ π₯} β ((cardββ© {π₯
β On β£ π΄ βΊ
π₯}) β V β β© {π₯
β On β£ π΄ βΊ
π₯} β
V)) |
48 | 46, 47 | mpbii 232 |
. . . . 5
β’
((cardββ© {π₯ β On β£ π΄ βΊ π₯}) = β© {π₯ β On β£ π΄ βΊ π₯} β β© {π₯ β On β£ π΄ βΊ π₯} β V) |
49 | 45, 48 | nsyl 140 |
. . . 4
β’ ({π₯ β On β£ π΄ βΊ π₯} = β
β Β¬ (cardββ© {π₯
β On β£ π΄ βΊ
π₯}) = β© {π₯
β On β£ π΄ βΊ
π₯}) |
50 | 49 | necon2ai 2970 |
. . 3
β’
((cardββ© {π₯ β On β£ π΄ βΊ π₯}) = β© {π₯ β On β£ π΄ βΊ π₯} β {π₯ β On β£ π΄ βΊ π₯} β β
) |
51 | | rabn0 4346 |
. . 3
β’ ({π₯ β On β£ π΄ βΊ π₯} β β
β βπ₯ β On π΄ βΊ π₯) |
52 | 50, 51 | sylib 217 |
. 2
β’
((cardββ© {π₯ β On β£ π΄ βΊ π₯}) = β© {π₯ β On β£ π΄ βΊ π₯} β βπ₯ β On π΄ βΊ π₯) |
53 | 39, 52 | impbii 208 |
1
β’
(βπ₯ β On
π΄ βΊ π₯ β (cardββ© {π₯
β On β£ π΄ βΊ
π₯}) = β© {π₯
β On β£ π΄ βΊ
π₯}) |