Step | Hyp | Ref
| Expression |
1 | | alephon 10013 |
. . . 4
β’
(β΅βπ¦)
β On |
2 | | pweq 4578 |
. . . . . 6
β’ (π₯ = (β΅βπ¦) β π« π₯ = π«
(β΅βπ¦)) |
3 | 2 | eleq1d 2819 |
. . . . 5
β’ (π₯ = (β΅βπ¦) β (π« π₯ β dom card β
π« (β΅βπ¦)
β dom card)) |
4 | 3 | rspcv 3579 |
. . . 4
β’
((β΅βπ¦)
β On β (βπ₯
β On π« π₯
β dom card β π« (β΅βπ¦) β dom card)) |
5 | 1, 4 | ax-mp 5 |
. . 3
β’
(βπ₯ β On
π« π₯ β dom card
β π« (β΅βπ¦) β dom card) |
6 | 5 | ralrimivw 3144 |
. 2
β’
(βπ₯ β On
π« π₯ β dom card
β βπ¦ β On
π« (β΅βπ¦)
β dom card) |
7 | | omelon 9590 |
. . . . . . 7
β’ Ο
β On |
8 | | cardon 9888 |
. . . . . . 7
β’
(cardβπ₯)
β On |
9 | | ontri1 6355 |
. . . . . . 7
β’ ((Ο
β On β§ (cardβπ₯) β On) β (Ο β
(cardβπ₯) β Β¬
(cardβπ₯) β
Ο)) |
10 | 7, 8, 9 | mp2an 691 |
. . . . . 6
β’ (Ο
β (cardβπ₯)
β Β¬ (cardβπ₯)
β Ο) |
11 | | cardidm 9903 |
. . . . . . . 8
β’
(cardβ(cardβπ₯)) = (cardβπ₯) |
12 | | cardalephex 10034 |
. . . . . . . 8
β’ (Ο
β (cardβπ₯)
β ((cardβ(cardβπ₯)) = (cardβπ₯) β βπ¦ β On (cardβπ₯) = (β΅βπ¦))) |
13 | 11, 12 | mpbii 232 |
. . . . . . 7
β’ (Ο
β (cardβπ₯)
β βπ¦ β On
(cardβπ₯) =
(β΅βπ¦)) |
14 | | r19.29 3114 |
. . . . . . . . 9
β’
((βπ¦ β
On π« (β΅βπ¦) β dom card β§ βπ¦ β On (cardβπ₯) = (β΅βπ¦)) β βπ¦ β On (π«
(β΅βπ¦) β
dom card β§ (cardβπ₯) = (β΅βπ¦))) |
15 | | pweq 4578 |
. . . . . . . . . . . 12
β’
((cardβπ₯) =
(β΅βπ¦) β
π« (cardβπ₯) =
π« (β΅βπ¦)) |
16 | 15 | eleq1d 2819 |
. . . . . . . . . . 11
β’
((cardβπ₯) =
(β΅βπ¦) β
(π« (cardβπ₯)
β dom card β π« (β΅βπ¦) β dom card)) |
17 | 16 | biimparc 481 |
. . . . . . . . . 10
β’
((π« (β΅βπ¦) β dom card β§ (cardβπ₯) = (β΅βπ¦)) β π«
(cardβπ₯) β dom
card) |
18 | 17 | rexlimivw 3145 |
. . . . . . . . 9
β’
(βπ¦ β On
(π« (β΅βπ¦) β dom card β§ (cardβπ₯) = (β΅βπ¦)) β π«
(cardβπ₯) β dom
card) |
19 | 14, 18 | syl 17 |
. . . . . . . 8
β’
((βπ¦ β
On π« (β΅βπ¦) β dom card β§ βπ¦ β On (cardβπ₯) = (β΅βπ¦)) β π«
(cardβπ₯) β dom
card) |
20 | 19 | ex 414 |
. . . . . . 7
β’
(βπ¦ β On
π« (β΅βπ¦)
β dom card β (βπ¦ β On (cardβπ₯) = (β΅βπ¦) β π« (cardβπ₯) β dom
card)) |
21 | 13, 20 | syl5 34 |
. . . . . 6
β’
(βπ¦ β On
π« (β΅βπ¦)
β dom card β (Ο β (cardβπ₯) β π« (cardβπ₯) β dom
card)) |
22 | 10, 21 | biimtrrid 242 |
. . . . 5
β’
(βπ¦ β On
π« (β΅βπ¦)
β dom card β (Β¬ (cardβπ₯) β Ο β π«
(cardβπ₯) β dom
card)) |
23 | | nnfi 9117 |
. . . . . . 7
β’
((cardβπ₯)
β Ο β (cardβπ₯) β Fin) |
24 | | pwfi 9128 |
. . . . . . 7
β’
((cardβπ₯)
β Fin β π« (cardβπ₯) β Fin) |
25 | 23, 24 | sylib 217 |
. . . . . 6
β’
((cardβπ₯)
β Ο β π« (cardβπ₯) β Fin) |
26 | | finnum 9892 |
. . . . . 6
β’
(π« (cardβπ₯) β Fin β π«
(cardβπ₯) β dom
card) |
27 | 25, 26 | syl 17 |
. . . . 5
β’
((cardβπ₯)
β Ο β π« (cardβπ₯) β dom card) |
28 | 22, 27 | pm2.61d2 181 |
. . . 4
β’
(βπ¦ β On
π« (β΅βπ¦)
β dom card β π« (cardβπ₯) β dom card) |
29 | | oncardid 9900 |
. . . . 5
β’ (π₯ β On β
(cardβπ₯) β
π₯) |
30 | | pwen 9100 |
. . . . 5
β’
((cardβπ₯)
β π₯ β π«
(cardβπ₯) β
π« π₯) |
31 | | ennum 9891 |
. . . . 5
β’
(π« (cardβπ₯) β π« π₯ β (π« (cardβπ₯) β dom card β
π« π₯ β dom
card)) |
32 | 29, 30, 31 | 3syl 18 |
. . . 4
β’ (π₯ β On β (π«
(cardβπ₯) β dom
card β π« π₯
β dom card)) |
33 | 28, 32 | syl5ibcom 244 |
. . 3
β’
(βπ¦ β On
π« (β΅βπ¦)
β dom card β (π₯
β On β π« π₯ β dom card)) |
34 | 33 | ralrimiv 3139 |
. 2
β’
(βπ¦ β On
π« (β΅βπ¦)
β dom card β βπ₯ β On π« π₯ β dom card) |
35 | 6, 34 | impbii 208 |
1
β’
(βπ₯ β On
π« π₯ β dom card
β βπ¦ β On
π« (β΅βπ¦)
β dom card) |