Step | Hyp | Ref
| Expression |
1 | | harcl 9553 |
. 2
β’
(harβπ΄) β
On |
2 | | harndom 9556 |
. . . . . . 7
β’ Β¬
(harβπ΄) βΌ π΄ |
3 | | simpll 764 |
. . . . . . . . 9
β’ (((π₯ β On β§
(harβπ΄) β π₯) β§ π¦ β (harβπ΄)) β π₯ β On) |
4 | | simpr 484 |
. . . . . . . . . . 11
β’ (((π₯ β On β§
(harβπ΄) β π₯) β§ π¦ β (harβπ΄)) β π¦ β (harβπ΄)) |
5 | | elharval 9555 |
. . . . . . . . . . 11
β’ (π¦ β (harβπ΄) β (π¦ β On β§ π¦ βΌ π΄)) |
6 | 4, 5 | sylib 217 |
. . . . . . . . . 10
β’ (((π₯ β On β§
(harβπ΄) β π₯) β§ π¦ β (harβπ΄)) β (π¦ β On β§ π¦ βΌ π΄)) |
7 | 6 | simpld 494 |
. . . . . . . . 9
β’ (((π₯ β On β§
(harβπ΄) β π₯) β§ π¦ β (harβπ΄)) β π¦ β On) |
8 | | ontri1 6391 |
. . . . . . . . 9
β’ ((π₯ β On β§ π¦ β On) β (π₯ β π¦ β Β¬ π¦ β π₯)) |
9 | 3, 7, 8 | syl2anc 583 |
. . . . . . . 8
β’ (((π₯ β On β§
(harβπ΄) β π₯) β§ π¦ β (harβπ΄)) β (π₯ β π¦ β Β¬ π¦ β π₯)) |
10 | | simpllr 773 |
. . . . . . . . . 10
β’ ((((π₯ β On β§
(harβπ΄) β π₯) β§ π¦ β (harβπ΄)) β§ π₯ β π¦) β (harβπ΄) β π₯) |
11 | | ssdomg 8995 |
. . . . . . . . . . . 12
β’ (π¦ β V β (π₯ β π¦ β π₯ βΌ π¦)) |
12 | 11 | elv 3474 |
. . . . . . . . . . 11
β’ (π₯ β π¦ β π₯ βΌ π¦) |
13 | 6 | simprd 495 |
. . . . . . . . . . 11
β’ (((π₯ β On β§
(harβπ΄) β π₯) β§ π¦ β (harβπ΄)) β π¦ βΌ π΄) |
14 | | domtr 9002 |
. . . . . . . . . . 11
β’ ((π₯ βΌ π¦ β§ π¦ βΌ π΄) β π₯ βΌ π΄) |
15 | 12, 13, 14 | syl2anr 596 |
. . . . . . . . . 10
β’ ((((π₯ β On β§
(harβπ΄) β π₯) β§ π¦ β (harβπ΄)) β§ π₯ β π¦) β π₯ βΌ π΄) |
16 | | endomtr 9007 |
. . . . . . . . . 10
β’
(((harβπ΄)
β π₯ β§ π₯ βΌ π΄) β (harβπ΄) βΌ π΄) |
17 | 10, 15, 16 | syl2anc 583 |
. . . . . . . . 9
β’ ((((π₯ β On β§
(harβπ΄) β π₯) β§ π¦ β (harβπ΄)) β§ π₯ β π¦) β (harβπ΄) βΌ π΄) |
18 | 17 | ex 412 |
. . . . . . . 8
β’ (((π₯ β On β§
(harβπ΄) β π₯) β§ π¦ β (harβπ΄)) β (π₯ β π¦ β (harβπ΄) βΌ π΄)) |
19 | 9, 18 | sylbird 260 |
. . . . . . 7
β’ (((π₯ β On β§
(harβπ΄) β π₯) β§ π¦ β (harβπ΄)) β (Β¬ π¦ β π₯ β (harβπ΄) βΌ π΄)) |
20 | 2, 19 | mt3i 149 |
. . . . . 6
β’ (((π₯ β On β§
(harβπ΄) β π₯) β§ π¦ β (harβπ΄)) β π¦ β π₯) |
21 | 20 | ex 412 |
. . . . 5
β’ ((π₯ β On β§
(harβπ΄) β π₯) β (π¦ β (harβπ΄) β π¦ β π₯)) |
22 | 21 | ssrdv 3983 |
. . . 4
β’ ((π₯ β On β§
(harβπ΄) β π₯) β (harβπ΄) β π₯) |
23 | 22 | ex 412 |
. . 3
β’ (π₯ β On β
((harβπ΄) β
π₯ β (harβπ΄) β π₯)) |
24 | 23 | rgen 3057 |
. 2
β’
βπ₯ β On
((harβπ΄) β
π₯ β (harβπ΄) β π₯) |
25 | | iscard2 9970 |
. 2
β’
((cardβ(harβπ΄)) = (harβπ΄) β ((harβπ΄) β On β§ βπ₯ β On ((harβπ΄) β π₯ β (harβπ΄) β π₯))) |
26 | 1, 24, 25 | mpbir2an 708 |
1
β’
(cardβ(harβπ΄)) = (harβπ΄) |