Step | Hyp | Ref
| Expression |
1 | | harcl 9554 |
. . . . . . . . . . . . . 14
β’
(harβπ΄) β
On |
2 | | sdomdom 8976 |
. . . . . . . . . . . . . 14
β’ (π₯ βΊ (harβπ΄) β π₯ βΌ (harβπ΄)) |
3 | | ondomen 10032 |
. . . . . . . . . . . . . 14
β’
(((harβπ΄)
β On β§ π₯ βΌ
(harβπ΄)) β π₯ β dom
card) |
4 | 1, 2, 3 | sylancr 588 |
. . . . . . . . . . . . 13
β’ (π₯ βΊ (harβπ΄) β π₯ β dom card) |
5 | | onenon 9944 |
. . . . . . . . . . . . . 14
β’
((harβπ΄)
β On β (harβπ΄) β dom card) |
6 | 1, 5 | ax-mp 5 |
. . . . . . . . . . . . 13
β’
(harβπ΄) β
dom card |
7 | | cardsdom2 9983 |
. . . . . . . . . . . . 13
β’ ((π₯ β dom card β§
(harβπ΄) β dom
card) β ((cardβπ₯) β (cardβ(harβπ΄)) β π₯ βΊ (harβπ΄))) |
8 | 4, 6, 7 | sylancl 587 |
. . . . . . . . . . . 12
β’ (π₯ βΊ (harβπ΄) β ((cardβπ₯) β
(cardβ(harβπ΄))
β π₯ βΊ
(harβπ΄))) |
9 | 8 | ibir 268 |
. . . . . . . . . . 11
β’ (π₯ βΊ (harβπ΄) β (cardβπ₯) β
(cardβ(harβπ΄))) |
10 | | harcard 9973 |
. . . . . . . . . . 11
β’
(cardβ(harβπ΄)) = (harβπ΄) |
11 | 9, 10 | eleqtrdi 2844 |
. . . . . . . . . 10
β’ (π₯ βΊ (harβπ΄) β (cardβπ₯) β (harβπ΄)) |
12 | | elharval 9556 |
. . . . . . . . . . 11
β’
((cardβπ₯)
β (harβπ΄) β
((cardβπ₯) β On
β§ (cardβπ₯)
βΌ π΄)) |
13 | 12 | simprbi 498 |
. . . . . . . . . 10
β’
((cardβπ₯)
β (harβπ΄) β
(cardβπ₯) βΌ
π΄) |
14 | 11, 13 | syl 17 |
. . . . . . . . 9
β’ (π₯ βΊ (harβπ΄) β (cardβπ₯) βΌ π΄) |
15 | | cardid2 9948 |
. . . . . . . . . 10
β’ (π₯ β dom card β
(cardβπ₯) β
π₯) |
16 | | domen1 9119 |
. . . . . . . . . 10
β’
((cardβπ₯)
β π₯ β
((cardβπ₯) βΌ
π΄ β π₯ βΌ π΄)) |
17 | 4, 15, 16 | 3syl 18 |
. . . . . . . . 9
β’ (π₯ βΊ (harβπ΄) β ((cardβπ₯) βΌ π΄ β π₯ βΌ π΄)) |
18 | 14, 17 | mpbid 231 |
. . . . . . . 8
β’ (π₯ βΊ (harβπ΄) β π₯ βΌ π΄) |
19 | | domnsym 9099 |
. . . . . . . 8
β’ (π₯ βΌ π΄ β Β¬ π΄ βΊ π₯) |
20 | 18, 19 | syl 17 |
. . . . . . 7
β’ (π₯ βΊ (harβπ΄) β Β¬ π΄ βΊ π₯) |
21 | 20 | con2i 139 |
. . . . . 6
β’ (π΄ βΊ π₯ β Β¬ π₯ βΊ (harβπ΄)) |
22 | | sdomen2 9122 |
. . . . . . 7
β’
((harβπ΄)
β π« π΄ β
(π₯ βΊ (harβπ΄) β π₯ βΊ π« π΄)) |
23 | 22 | notbid 318 |
. . . . . 6
β’
((harβπ΄)
β π« π΄ β
(Β¬ π₯ βΊ
(harβπ΄) β Β¬
π₯ βΊ π« π΄)) |
24 | 21, 23 | imbitrid 243 |
. . . . 5
β’
((harβπ΄)
β π« π΄ β
(π΄ βΊ π₯ β Β¬ π₯ βΊ π« π΄)) |
25 | | imnan 401 |
. . . . 5
β’ ((π΄ βΊ π₯ β Β¬ π₯ βΊ π« π΄) β Β¬ (π΄ βΊ π₯ β§ π₯ βΊ π« π΄)) |
26 | 24, 25 | sylib 217 |
. . . 4
β’
((harβπ΄)
β π« π΄ β
Β¬ (π΄ βΊ π₯ β§ π₯ βΊ π« π΄)) |
27 | 26 | alrimiv 1931 |
. . 3
β’
((harβπ΄)
β π« π΄ β
βπ₯ Β¬ (π΄ βΊ π₯ β§ π₯ βΊ π« π΄)) |
28 | 27 | olcd 873 |
. 2
β’
((harβπ΄)
β π« π΄ β
(π΄ β Fin β¨
βπ₯ Β¬ (π΄ βΊ π₯ β§ π₯ βΊ π« π΄))) |
29 | | relen 8944 |
. . . . 5
β’ Rel
β |
30 | 29 | brrelex2i 5734 |
. . . 4
β’
((harβπ΄)
β π« π΄ β
π« π΄ β
V) |
31 | | pwexb 7753 |
. . . 4
β’ (π΄ β V β π« π΄ β V) |
32 | 30, 31 | sylibr 233 |
. . 3
β’
((harβπ΄)
β π« π΄ β
π΄ β
V) |
33 | | elgch 10617 |
. . 3
β’ (π΄ β V β (π΄ β GCH β (π΄ β Fin β¨ βπ₯ Β¬ (π΄ βΊ π₯ β§ π₯ βΊ π« π΄)))) |
34 | 32, 33 | syl 17 |
. 2
β’
((harβπ΄)
β π« π΄ β
(π΄ β GCH β (π΄ β Fin β¨ βπ₯ Β¬ (π΄ βΊ π₯ β§ π₯ βΊ π« π΄)))) |
35 | 28, 34 | mpbird 257 |
1
β’
((harβπ΄)
β π« π΄ β
π΄ β
GCH) |