Step | Hyp | Ref
| Expression |
1 | | ssonuni 7715 |
. . . . 5
β’ (π΄ β π β (π΄ β On β βͺ π΄
β On)) |
2 | | fveq2 6843 |
. . . . . . . . 9
β’ (π₯ = π¦ β (cardβπ₯) = (cardβπ¦)) |
3 | | id 22 |
. . . . . . . . 9
β’ (π₯ = π¦ β π₯ = π¦) |
4 | 2, 3 | eqeq12d 2749 |
. . . . . . . 8
β’ (π₯ = π¦ β ((cardβπ₯) = π₯ β (cardβπ¦) = π¦)) |
5 | 4 | rspcv 3576 |
. . . . . . 7
β’ (π¦ β π΄ β (βπ₯ β π΄ (cardβπ₯) = π₯ β (cardβπ¦) = π¦)) |
6 | | cardon 9885 |
. . . . . . . 8
β’
(cardβπ¦)
β On |
7 | | eleq1 2822 |
. . . . . . . 8
β’
((cardβπ¦) =
π¦ β ((cardβπ¦) β On β π¦ β On)) |
8 | 6, 7 | mpbii 232 |
. . . . . . 7
β’
((cardβπ¦) =
π¦ β π¦ β On) |
9 | 5, 8 | syl6com 37 |
. . . . . 6
β’
(βπ₯ β
π΄ (cardβπ₯) = π₯ β (π¦ β π΄ β π¦ β On)) |
10 | 9 | ssrdv 3951 |
. . . . 5
β’
(βπ₯ β
π΄ (cardβπ₯) = π₯ β π΄ β On) |
11 | 1, 10 | impel 507 |
. . . 4
β’ ((π΄ β π β§ βπ₯ β π΄ (cardβπ₯) = π₯) β βͺ π΄ β On) |
12 | | cardonle 9898 |
. . . 4
β’ (βͺ π΄
β On β (cardββͺ π΄) β βͺ π΄) |
13 | 11, 12 | syl 17 |
. . 3
β’ ((π΄ β π β§ βπ₯ β π΄ (cardβπ₯) = π₯) β (cardββͺ π΄)
β βͺ π΄) |
14 | | cardon 9885 |
. . . . 5
β’
(cardββͺ π΄) β On |
15 | 14 | onirri 6431 |
. . . 4
β’ Β¬
(cardββͺ π΄) β (cardββͺ π΄) |
16 | | eluni 4869 |
. . . . . . . 8
β’
((cardββͺ π΄) β βͺ π΄ β βπ¦((cardββͺ π΄)
β π¦ β§ π¦ β π΄)) |
17 | | elssuni 4899 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β π΄ β π¦ β βͺ π΄) |
18 | | ssdomg 8943 |
. . . . . . . . . . . . . . . . . . 19
β’ (βͺ π΄
β On β (π¦ β
βͺ π΄ β π¦ βΌ βͺ π΄)) |
19 | 18 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’
(((cardβπ¦) =
π¦ β§ βͺ π΄
β On) β (π¦
β βͺ π΄ β π¦ βΌ βͺ π΄)) |
20 | 17, 19 | syl5 34 |
. . . . . . . . . . . . . . . . 17
β’
(((cardβπ¦) =
π¦ β§ βͺ π΄
β On) β (π¦ β
π΄ β π¦ βΌ βͺ π΄)) |
21 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
β’
((cardβπ¦) =
π¦ β (cardβπ¦) = π¦) |
22 | | onenon 9890 |
. . . . . . . . . . . . . . . . . . . 20
β’
((cardβπ¦)
β On β (cardβπ¦) β dom card) |
23 | 6, 22 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
β’
(cardβπ¦)
β dom card |
24 | 21, 23 | eqeltrrdi 2843 |
. . . . . . . . . . . . . . . . . 18
β’
((cardβπ¦) =
π¦ β π¦ β dom card) |
25 | | onenon 9890 |
. . . . . . . . . . . . . . . . . 18
β’ (βͺ π΄
β On β βͺ π΄ β dom card) |
26 | | carddom2 9918 |
. . . . . . . . . . . . . . . . . 18
β’ ((π¦ β dom card β§ βͺ π΄
β dom card) β ((cardβπ¦) β (cardββͺ π΄)
β π¦ βΌ βͺ π΄)) |
27 | 24, 25, 26 | syl2an 597 |
. . . . . . . . . . . . . . . . 17
β’
(((cardβπ¦) =
π¦ β§ βͺ π΄
β On) β ((cardβπ¦) β (cardββͺ π΄)
β π¦ βΌ βͺ π΄)) |
28 | 20, 27 | sylibrd 259 |
. . . . . . . . . . . . . . . 16
β’
(((cardβπ¦) =
π¦ β§ βͺ π΄
β On) β (π¦ β
π΄ β (cardβπ¦) β (cardββͺ π΄))) |
29 | | sseq1 3970 |
. . . . . . . . . . . . . . . . 17
β’
((cardβπ¦) =
π¦ β ((cardβπ¦) β (cardββͺ π΄)
β π¦ β
(cardββͺ π΄))) |
30 | 29 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
(((cardβπ¦) =
π¦ β§ βͺ π΄
β On) β ((cardβπ¦) β (cardββͺ π΄)
β π¦ β
(cardββͺ π΄))) |
31 | 28, 30 | sylibd 238 |
. . . . . . . . . . . . . . 15
β’
(((cardβπ¦) =
π¦ β§ βͺ π΄
β On) β (π¦ β
π΄ β π¦ β (cardββͺ π΄))) |
32 | | ssel 3938 |
. . . . . . . . . . . . . . 15
β’ (π¦ β (cardββͺ π΄)
β ((cardββͺ π΄) β π¦ β (cardββͺ π΄)
β (cardββͺ π΄))) |
33 | 31, 32 | syl6 35 |
. . . . . . . . . . . . . 14
β’
(((cardβπ¦) =
π¦ β§ βͺ π΄
β On) β (π¦ β
π΄ β ((cardββͺ π΄)
β π¦ β
(cardββͺ π΄) β (cardββͺ π΄)))) |
34 | 33 | ex 414 |
. . . . . . . . . . . . 13
β’
((cardβπ¦) =
π¦ β (βͺ π΄
β On β (π¦ β
π΄ β ((cardββͺ π΄)
β π¦ β
(cardββͺ π΄) β (cardββͺ π΄))))) |
35 | 34 | com3r 87 |
. . . . . . . . . . . 12
β’ (π¦ β π΄ β ((cardβπ¦) = π¦ β (βͺ π΄ β On β
((cardββͺ π΄) β π¦ β (cardββͺ π΄)
β (cardββͺ π΄))))) |
36 | 5, 35 | syld 47 |
. . . . . . . . . . 11
β’ (π¦ β π΄ β (βπ₯ β π΄ (cardβπ₯) = π₯ β (βͺ π΄ β On β
((cardββͺ π΄) β π¦ β (cardββͺ π΄)
β (cardββͺ π΄))))) |
37 | 36 | com4r 94 |
. . . . . . . . . 10
β’
((cardββͺ π΄) β π¦ β (π¦ β π΄ β (βπ₯ β π΄ (cardβπ₯) = π₯ β (βͺ π΄ β On β
(cardββͺ π΄) β (cardββͺ π΄))))) |
38 | 37 | imp 408 |
. . . . . . . . 9
β’
(((cardββͺ π΄) β π¦ β§ π¦ β π΄) β (βπ₯ β π΄ (cardβπ₯) = π₯ β (βͺ π΄ β On β
(cardββͺ π΄) β (cardββͺ π΄)))) |
39 | 38 | exlimiv 1934 |
. . . . . . . 8
β’
(βπ¦((cardββͺ
π΄) β π¦ β§ π¦ β π΄) β (βπ₯ β π΄ (cardβπ₯) = π₯ β (βͺ π΄ β On β
(cardββͺ π΄) β (cardββͺ π΄)))) |
40 | 16, 39 | sylbi 216 |
. . . . . . 7
β’
((cardββͺ π΄) β βͺ π΄ β (βπ₯ β π΄ (cardβπ₯) = π₯ β (βͺ π΄ β On β
(cardββͺ π΄) β (cardββͺ π΄)))) |
41 | 40 | com13 88 |
. . . . . 6
β’ (βͺ π΄
β On β (βπ₯
β π΄ (cardβπ₯) = π₯ β ((cardββͺ π΄)
β βͺ π΄ β (cardββͺ π΄)
β (cardββͺ π΄)))) |
42 | 41 | imp 408 |
. . . . 5
β’ ((βͺ π΄
β On β§ βπ₯
β π΄ (cardβπ₯) = π₯) β ((cardββͺ π΄)
β βͺ π΄ β (cardββͺ π΄)
β (cardββͺ π΄))) |
43 | 11, 42 | sylancom 589 |
. . . 4
β’ ((π΄ β π β§ βπ₯ β π΄ (cardβπ₯) = π₯) β ((cardββͺ π΄)
β βͺ π΄ β (cardββͺ π΄)
β (cardββͺ π΄))) |
44 | 15, 43 | mtoi 198 |
. . 3
β’ ((π΄ β π β§ βπ₯ β π΄ (cardβπ₯) = π₯) β Β¬ (cardββͺ π΄)
β βͺ π΄) |
45 | 14 | onordi 6429 |
. . . 4
β’ Ord
(cardββͺ π΄) |
46 | | eloni 6328 |
. . . . 5
β’ (βͺ π΄
β On β Ord βͺ π΄) |
47 | 11, 46 | syl 17 |
. . . 4
β’ ((π΄ β π β§ βπ₯ β π΄ (cardβπ₯) = π₯) β Ord βͺ
π΄) |
48 | | ordtri4 6355 |
. . . 4
β’ ((Ord
(cardββͺ π΄) β§ Ord βͺ
π΄) β
((cardββͺ π΄) = βͺ π΄ β ((cardββͺ π΄)
β βͺ π΄ β§ Β¬ (cardββͺ π΄)
β βͺ π΄))) |
49 | 45, 47, 48 | sylancr 588 |
. . 3
β’ ((π΄ β π β§ βπ₯ β π΄ (cardβπ₯) = π₯) β ((cardββͺ π΄) =
βͺ π΄ β ((cardββͺ π΄)
β βͺ π΄ β§ Β¬ (cardββͺ π΄)
β βͺ π΄))) |
50 | 13, 44, 49 | mpbir2and 712 |
. 2
β’ ((π΄ β π β§ βπ₯ β π΄ (cardβπ₯) = π₯) β (cardββͺ π΄) =
βͺ π΄) |
51 | 50 | ex 414 |
1
β’ (π΄ β π β (βπ₯ β π΄ (cardβπ₯) = π₯ β (cardββͺ π΄) =
βͺ π΄)) |