Step | Hyp | Ref
| Expression |
1 | | fvex 6856 |
. . . 4
β’
(cardβ(βͺ π΄ β π΅)) β V |
2 | 1 | sucid 6400 |
. . 3
β’
(cardβ(βͺ π΄ β π΅)) β suc (cardβ(βͺ π΄
β π΅)) |
3 | | ttukeylem.1 |
. . . 4
β’ (π β πΉ:(cardβ(βͺ
π΄ β π΅))β1-1-ontoβ(βͺ π΄ β π΅)) |
4 | | ttukeylem.2 |
. . . 4
β’ (π β π΅ β π΄) |
5 | | ttukeylem.3 |
. . . 4
β’ (π β βπ₯(π₯ β π΄ β (π« π₯ β© Fin) β π΄)) |
6 | | ttukeylem.4 |
. . . 4
β’ πΊ = recs((π§ β V β¦ if(dom π§ = βͺ dom π§, if(dom π§ = β
, π΅, βͺ ran π§), ((π§ββͺ dom π§) βͺ if(((π§ββͺ dom π§) βͺ {(πΉββͺ dom
π§)}) β π΄, {(πΉββͺ dom
π§)},
β
))))) |
7 | 3, 4, 5, 6 | ttukeylem6 10451 |
. . 3
β’ ((π β§ (cardβ(βͺ π΄
β π΅)) β suc
(cardβ(βͺ π΄ β π΅))) β (πΊβ(cardβ(βͺ π΄
β π΅))) β π΄) |
8 | 2, 7 | mpan2 690 |
. 2
β’ (π β (πΊβ(cardβ(βͺ π΄
β π΅))) β π΄) |
9 | 3, 4, 5, 6 | ttukeylem4 10449 |
. . 3
β’ (π β (πΊββ
) = π΅) |
10 | | 0elon 6372 |
. . . . 5
β’ β
β On |
11 | | cardon 9881 |
. . . . 5
β’
(cardβ(βͺ π΄ β π΅)) β On |
12 | | 0ss 4357 |
. . . . 5
β’ β
β (cardβ(βͺ π΄ β π΅)) |
13 | 10, 11, 12 | 3pm3.2i 1340 |
. . . 4
β’ (β
β On β§ (cardβ(βͺ π΄ β π΅)) β On β§ β
β
(cardβ(βͺ π΄ β π΅))) |
14 | 3, 4, 5, 6 | ttukeylem5 10450 |
. . . 4
β’ ((π β§ (β
β On β§
(cardβ(βͺ π΄ β π΅)) β On β§ β
β
(cardβ(βͺ π΄ β π΅)))) β (πΊββ
) β (πΊβ(cardβ(βͺ π΄
β π΅)))) |
15 | 13, 14 | mpan2 690 |
. . 3
β’ (π β (πΊββ
) β (πΊβ(cardβ(βͺ π΄
β π΅)))) |
16 | 9, 15 | eqsstrrd 3984 |
. 2
β’ (π β π΅ β (πΊβ(cardβ(βͺ π΄
β π΅)))) |
17 | | simprr 772 |
. . . . . 6
β’ ((π β§ (π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦)) β (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) |
18 | | ssun1 4133 |
. . . . . . . 8
β’ π¦ β (π¦ βͺ π΅) |
19 | | undif1 4436 |
. . . . . . . 8
β’ ((π¦ β π΅) βͺ π΅) = (π¦ βͺ π΅) |
20 | 18, 19 | sseqtrri 3982 |
. . . . . . 7
β’ π¦ β ((π¦ β π΅) βͺ π΅) |
21 | | simpl 484 |
. . . . . . . . . . . 12
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β π) |
22 | | f1ocnv 6797 |
. . . . . . . . . . . . . . . . 17
β’ (πΉ:(cardβ(βͺ π΄
β π΅))β1-1-ontoβ(βͺ π΄ β π΅) β β‘πΉ:(βͺ π΄ β π΅)β1-1-ontoβ(cardβ(βͺ
π΄ β π΅))) |
23 | | f1of 6785 |
. . . . . . . . . . . . . . . . 17
β’ (β‘πΉ:(βͺ π΄ β π΅)β1-1-ontoβ(cardβ(βͺ
π΄ β π΅)) β β‘πΉ:(βͺ π΄ β π΅)βΆ(cardβ(βͺ π΄
β π΅))) |
24 | 3, 22, 23 | 3syl 18 |
. . . . . . . . . . . . . . . 16
β’ (π β β‘πΉ:(βͺ π΄ β π΅)βΆ(cardβ(βͺ π΄
β π΅))) |
25 | 24 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β β‘πΉ:(βͺ π΄ β π΅)βΆ(cardβ(βͺ π΄
β π΅))) |
26 | | eldifi 4087 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π¦ β π΅) β π β π¦) |
27 | 26 | ad2antll 728 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β π β π¦) |
28 | | simprll 778 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β π¦ β π΄) |
29 | | elunii 4871 |
. . . . . . . . . . . . . . . . 17
β’ ((π β π¦ β§ π¦ β π΄) β π β βͺ π΄) |
30 | 27, 28, 29 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β π β βͺ π΄) |
31 | | eldifn 4088 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π¦ β π΅) β Β¬ π β π΅) |
32 | 31 | ad2antll 728 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β Β¬ π β π΅) |
33 | 30, 32 | eldifd 3922 |
. . . . . . . . . . . . . . 15
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β π β (βͺ π΄ β π΅)) |
34 | 25, 33 | ffvelcdmd 7037 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β (β‘πΉβπ) β (cardβ(βͺ π΄
β π΅))) |
35 | | onelon 6343 |
. . . . . . . . . . . . . 14
β’
(((cardβ(βͺ π΄ β π΅)) β On β§ (β‘πΉβπ) β (cardβ(βͺ π΄
β π΅))) β (β‘πΉβπ) β On) |
36 | 11, 34, 35 | sylancr 588 |
. . . . . . . . . . . . 13
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β (β‘πΉβπ) β On) |
37 | | onsuc 7747 |
. . . . . . . . . . . . 13
β’ ((β‘πΉβπ) β On β suc (β‘πΉβπ) β On) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β suc (β‘πΉβπ) β On) |
39 | 11 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β (cardβ(βͺ π΄
β π΅)) β
On) |
40 | 11 | onordi 6429 |
. . . . . . . . . . . . 13
β’ Ord
(cardβ(βͺ π΄ β π΅)) |
41 | | ordsucss 7754 |
. . . . . . . . . . . . 13
β’ (Ord
(cardβ(βͺ π΄ β π΅)) β ((β‘πΉβπ) β (cardβ(βͺ π΄
β π΅)) β suc
(β‘πΉβπ) β (cardβ(βͺ π΄
β π΅)))) |
42 | 40, 34, 41 | mpsyl 68 |
. . . . . . . . . . . 12
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β suc (β‘πΉβπ) β (cardβ(βͺ π΄
β π΅))) |
43 | 3, 4, 5, 6 | ttukeylem5 10450 |
. . . . . . . . . . . 12
β’ ((π β§ (suc (β‘πΉβπ) β On β§ (cardβ(βͺ π΄
β π΅)) β On β§
suc (β‘πΉβπ) β (cardβ(βͺ π΄
β π΅)))) β (πΊβsuc (β‘πΉβπ)) β (πΊβ(cardβ(βͺ π΄
β π΅)))) |
44 | 21, 38, 39, 42, 43 | syl13anc 1373 |
. . . . . . . . . . 11
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β (πΊβsuc (β‘πΉβπ)) β (πΊβ(cardβ(βͺ π΄
β π΅)))) |
45 | | ssun2 4134 |
. . . . . . . . . . . . 13
β’
if(((πΊββͺ suc (β‘πΉβπ)) βͺ {(πΉββͺ suc
(β‘πΉβπ))}) β π΄, {(πΉββͺ suc
(β‘πΉβπ))}, β
) β ((πΊββͺ suc
(β‘πΉβπ)) βͺ if(((πΊββͺ suc
(β‘πΉβπ)) βͺ {(πΉββͺ suc
(β‘πΉβπ))}) β π΄, {(πΉββͺ suc
(β‘πΉβπ))}, β
)) |
46 | | eloni 6328 |
. . . . . . . . . . . . . . . . . 18
β’ ((β‘πΉβπ) β On β Ord (β‘πΉβπ)) |
47 | | ordunisuc 7768 |
. . . . . . . . . . . . . . . . . 18
β’ (Ord
(β‘πΉβπ) β βͺ suc
(β‘πΉβπ) = (β‘πΉβπ)) |
48 | 36, 46, 47 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β βͺ suc
(β‘πΉβπ) = (β‘πΉβπ)) |
49 | 48 | fveq2d 6847 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β (πΉββͺ suc
(β‘πΉβπ)) = (πΉβ(β‘πΉβπ))) |
50 | 3 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β πΉ:(cardβ(βͺ
π΄ β π΅))β1-1-ontoβ(βͺ π΄ β π΅)) |
51 | | f1ocnvfv2 7224 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉ:(cardβ(βͺ π΄
β π΅))β1-1-ontoβ(βͺ π΄ β π΅) β§ π β (βͺ π΄ β π΅)) β (πΉβ(β‘πΉβπ)) = π) |
52 | 50, 33, 51 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β (πΉβ(β‘πΉβπ)) = π) |
53 | 49, 52 | eqtr2d 2778 |
. . . . . . . . . . . . . . 15
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β π = (πΉββͺ suc
(β‘πΉβπ))) |
54 | | velsn 4603 |
. . . . . . . . . . . . . . 15
β’ (π β {(πΉββͺ suc
(β‘πΉβπ))} β π = (πΉββͺ suc
(β‘πΉβπ))) |
55 | 53, 54 | sylibr 233 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β π β {(πΉββͺ suc
(β‘πΉβπ))}) |
56 | 48 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β (πΊββͺ suc
(β‘πΉβπ)) = (πΊβ(β‘πΉβπ))) |
57 | | ordelss 6334 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((Ord
(cardβ(βͺ π΄ β π΅)) β§ (β‘πΉβπ) β (cardβ(βͺ π΄
β π΅))) β (β‘πΉβπ) β (cardβ(βͺ π΄
β π΅))) |
58 | 40, 34, 57 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β (β‘πΉβπ) β (cardβ(βͺ π΄
β π΅))) |
59 | 3, 4, 5, 6 | ttukeylem5 10450 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ ((β‘πΉβπ) β On β§ (cardβ(βͺ π΄
β π΅)) β On β§
(β‘πΉβπ) β (cardβ(βͺ π΄
β π΅)))) β (πΊβ(β‘πΉβπ)) β (πΊβ(cardβ(βͺ π΄
β π΅)))) |
60 | 21, 36, 39, 58, 59 | syl13anc 1373 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β (πΊβ(β‘πΉβπ)) β (πΊβ(cardβ(βͺ π΄
β π΅)))) |
61 | 56, 60 | eqsstrd 3983 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β (πΊββͺ suc
(β‘πΉβπ)) β (πΊβ(cardβ(βͺ π΄
β π΅)))) |
62 | | simprlr 779 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) |
63 | 61, 62 | sstrd 3955 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β (πΊββͺ suc
(β‘πΉβπ)) β π¦) |
64 | 53, 27 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β (πΉββͺ suc
(β‘πΉβπ)) β π¦) |
65 | 64 | snssd 4770 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β {(πΉββͺ suc
(β‘πΉβπ))} β π¦) |
66 | 63, 65 | unssd 4147 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β ((πΊββͺ suc
(β‘πΉβπ)) βͺ {(πΉββͺ suc
(β‘πΉβπ))}) β π¦) |
67 | 3, 4, 5 | ttukeylem2 10447 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π¦ β π΄ β§ ((πΊββͺ suc
(β‘πΉβπ)) βͺ {(πΉββͺ suc
(β‘πΉβπ))}) β π¦)) β ((πΊββͺ suc
(β‘πΉβπ)) βͺ {(πΉββͺ suc
(β‘πΉβπ))}) β π΄) |
68 | 21, 28, 66, 67 | syl12anc 836 |
. . . . . . . . . . . . . . 15
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β ((πΊββͺ suc
(β‘πΉβπ)) βͺ {(πΉββͺ suc
(β‘πΉβπ))}) β π΄) |
69 | 68 | iftrued 4495 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β if(((πΊββͺ suc
(β‘πΉβπ)) βͺ {(πΉββͺ suc
(β‘πΉβπ))}) β π΄, {(πΉββͺ suc
(β‘πΉβπ))}, β
) = {(πΉββͺ suc
(β‘πΉβπ))}) |
70 | 55, 69 | eleqtrrd 2841 |
. . . . . . . . . . . . 13
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β π β if(((πΊββͺ suc
(β‘πΉβπ)) βͺ {(πΉββͺ suc
(β‘πΉβπ))}) β π΄, {(πΉββͺ suc
(β‘πΉβπ))}, β
)) |
71 | 45, 70 | sselid 3943 |
. . . . . . . . . . . 12
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β π β ((πΊββͺ suc
(β‘πΉβπ)) βͺ if(((πΊββͺ suc
(β‘πΉβπ)) βͺ {(πΉββͺ suc
(β‘πΉβπ))}) β π΄, {(πΉββͺ suc
(β‘πΉβπ))}, β
))) |
72 | 3, 4, 5, 6 | ttukeylem3 10448 |
. . . . . . . . . . . . . 14
β’ ((π β§ suc (β‘πΉβπ) β On) β (πΊβsuc (β‘πΉβπ)) = if(suc (β‘πΉβπ) = βͺ suc (β‘πΉβπ), if(suc (β‘πΉβπ) = β
, π΅, βͺ (πΊ β suc (β‘πΉβπ))), ((πΊββͺ suc
(β‘πΉβπ)) βͺ if(((πΊββͺ suc
(β‘πΉβπ)) βͺ {(πΉββͺ suc
(β‘πΉβπ))}) β π΄, {(πΉββͺ suc
(β‘πΉβπ))}, β
)))) |
73 | 38, 72 | syldan 592 |
. . . . . . . . . . . . 13
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β (πΊβsuc (β‘πΉβπ)) = if(suc (β‘πΉβπ) = βͺ suc (β‘πΉβπ), if(suc (β‘πΉβπ) = β
, π΅, βͺ (πΊ β suc (β‘πΉβπ))), ((πΊββͺ suc
(β‘πΉβπ)) βͺ if(((πΊββͺ suc
(β‘πΉβπ)) βͺ {(πΉββͺ suc
(β‘πΉβπ))}) β π΄, {(πΉββͺ suc
(β‘πΉβπ))}, β
)))) |
74 | | sucidg 6399 |
. . . . . . . . . . . . . . . . . 18
β’ ((β‘πΉβπ) β (cardβ(βͺ π΄
β π΅)) β (β‘πΉβπ) β suc (β‘πΉβπ)) |
75 | 34, 74 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β (β‘πΉβπ) β suc (β‘πΉβπ)) |
76 | | ordirr 6336 |
. . . . . . . . . . . . . . . . . 18
β’ (Ord
(β‘πΉβπ) β Β¬ (β‘πΉβπ) β (β‘πΉβπ)) |
77 | 36, 46, 76 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β Β¬ (β‘πΉβπ) β (β‘πΉβπ)) |
78 | | nelne1 3042 |
. . . . . . . . . . . . . . . . 17
β’ (((β‘πΉβπ) β suc (β‘πΉβπ) β§ Β¬ (β‘πΉβπ) β (β‘πΉβπ)) β suc (β‘πΉβπ) β (β‘πΉβπ)) |
79 | 75, 77, 78 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β suc (β‘πΉβπ) β (β‘πΉβπ)) |
80 | 79, 48 | neeqtrrd 3019 |
. . . . . . . . . . . . . . 15
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β suc (β‘πΉβπ) β βͺ suc
(β‘πΉβπ)) |
81 | 80 | neneqd 2949 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β Β¬ suc (β‘πΉβπ) = βͺ suc (β‘πΉβπ)) |
82 | 81 | iffalsed 4498 |
. . . . . . . . . . . . 13
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β if(suc (β‘πΉβπ) = βͺ suc (β‘πΉβπ), if(suc (β‘πΉβπ) = β
, π΅, βͺ (πΊ β suc (β‘πΉβπ))), ((πΊββͺ suc
(β‘πΉβπ)) βͺ if(((πΊββͺ suc
(β‘πΉβπ)) βͺ {(πΉββͺ suc
(β‘πΉβπ))}) β π΄, {(πΉββͺ suc
(β‘πΉβπ))}, β
))) = ((πΊββͺ suc
(β‘πΉβπ)) βͺ if(((πΊββͺ suc
(β‘πΉβπ)) βͺ {(πΉββͺ suc
(β‘πΉβπ))}) β π΄, {(πΉββͺ suc
(β‘πΉβπ))}, β
))) |
83 | 73, 82 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β (πΊβsuc (β‘πΉβπ)) = ((πΊββͺ suc
(β‘πΉβπ)) βͺ if(((πΊββͺ suc
(β‘πΉβπ)) βͺ {(πΉββͺ suc
(β‘πΉβπ))}) β π΄, {(πΉββͺ suc
(β‘πΉβπ))}, β
))) |
84 | 71, 83 | eleqtrrd 2841 |
. . . . . . . . . . 11
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β π β (πΊβsuc (β‘πΉβπ))) |
85 | 44, 84 | sseldd 3946 |
. . . . . . . . . 10
β’ ((π β§ ((π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) β§ π β (π¦ β π΅))) β π β (πΊβ(cardβ(βͺ π΄
β π΅)))) |
86 | 85 | expr 458 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦)) β (π β (π¦ β π΅) β π β (πΊβ(cardβ(βͺ π΄
β π΅))))) |
87 | 86 | ssrdv 3951 |
. . . . . . . 8
β’ ((π β§ (π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦)) β (π¦ β π΅) β (πΊβ(cardβ(βͺ π΄
β π΅)))) |
88 | 16 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦)) β π΅ β (πΊβ(cardβ(βͺ π΄
β π΅)))) |
89 | 87, 88 | unssd 4147 |
. . . . . . 7
β’ ((π β§ (π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦)) β ((π¦ β π΅) βͺ π΅) β (πΊβ(cardβ(βͺ π΄
β π΅)))) |
90 | 20, 89 | sstrid 3956 |
. . . . . 6
β’ ((π β§ (π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦)) β π¦ β (πΊβ(cardβ(βͺ π΄
β π΅)))) |
91 | 17, 90 | eqssd 3962 |
. . . . 5
β’ ((π β§ (π¦ β π΄ β§ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦)) β (πΊβ(cardβ(βͺ π΄
β π΅))) = π¦) |
92 | 91 | expr 458 |
. . . 4
β’ ((π β§ π¦ β π΄) β ((πΊβ(cardβ(βͺ π΄
β π΅))) β π¦ β (πΊβ(cardβ(βͺ π΄
β π΅))) = π¦)) |
93 | | npss 4071 |
. . . 4
β’ (Β¬
(πΊβ(cardβ(βͺ π΄
β π΅))) β π¦ β ((πΊβ(cardβ(βͺ π΄
β π΅))) β π¦ β (πΊβ(cardβ(βͺ π΄
β π΅))) = π¦)) |
94 | 92, 93 | sylibr 233 |
. . 3
β’ ((π β§ π¦ β π΄) β Β¬ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) |
95 | 94 | ralrimiva 3144 |
. 2
β’ (π β βπ¦ β π΄ Β¬ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦) |
96 | | sseq2 3971 |
. . . 4
β’ (π₯ = (πΊβ(cardβ(βͺ π΄
β π΅))) β (π΅ β π₯ β π΅ β (πΊβ(cardβ(βͺ π΄
β π΅))))) |
97 | | psseq1 4048 |
. . . . . 6
β’ (π₯ = (πΊβ(cardβ(βͺ π΄
β π΅))) β (π₯ β π¦ β (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦)) |
98 | 97 | notbid 318 |
. . . . 5
β’ (π₯ = (πΊβ(cardβ(βͺ π΄
β π΅))) β (Β¬
π₯ β π¦ β Β¬ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦)) |
99 | 98 | ralbidv 3175 |
. . . 4
β’ (π₯ = (πΊβ(cardβ(βͺ π΄
β π΅))) β
(βπ¦ β π΄ Β¬ π₯ β π¦ β βπ¦ β π΄ Β¬ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦)) |
100 | 96, 99 | anbi12d 632 |
. . 3
β’ (π₯ = (πΊβ(cardβ(βͺ π΄
β π΅))) β ((π΅ β π₯ β§ βπ¦ β π΄ Β¬ π₯ β π¦) β (π΅ β (πΊβ(cardβ(βͺ π΄
β π΅))) β§
βπ¦ β π΄ Β¬ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦))) |
101 | 100 | rspcev 3582 |
. 2
β’ (((πΊβ(cardβ(βͺ π΄
β π΅))) β π΄ β§ (π΅ β (πΊβ(cardβ(βͺ π΄
β π΅))) β§
βπ¦ β π΄ Β¬ (πΊβ(cardβ(βͺ π΄
β π΅))) β π¦)) β βπ₯ β π΄ (π΅ β π₯ β§ βπ¦ β π΄ Β¬ π₯ β π¦)) |
102 | 8, 16, 95, 101 | syl12anc 836 |
1
β’ (π β βπ₯ β π΄ (π΅ β π₯ β§ βπ¦ β π΄ Β¬ π₯ β π¦)) |