Step | Hyp | Ref
| Expression |
1 | | suceq 6387 |
. . . . 5
β’ (π = β
β suc π = suc β
) |
2 | 1 | raleqdv 3312 |
. . . 4
β’ (π = β
β (βπ β suc π(π΅βπ) β π« π β βπ β suc β
(π΅βπ) β π« π)) |
3 | | iuneq1 4974 |
. . . . 5
β’ (π = β
β βͺ π β π (π΅βπ) = βͺ π β β
(π΅βπ)) |
4 | | fveq2 6846 |
. . . . 5
β’ (π = β
β (π΅βπ) = (π΅ββ
)) |
5 | 3, 4 | breq12d 5122 |
. . . 4
β’ (π = β
β (βͺ π β π (π΅βπ) βΊ (π΅βπ) β βͺ
π β β
(π΅βπ) βΊ (π΅ββ
))) |
6 | 2, 5 | imbi12d 345 |
. . 3
β’ (π = β
β
((βπ β suc
π(π΅βπ) β π« π β βͺ
π β π (π΅βπ) βΊ (π΅βπ)) β (βπ β suc β
(π΅βπ) β π« π β βͺ
π β β
(π΅βπ) βΊ (π΅ββ
)))) |
7 | | suceq 6387 |
. . . . 5
β’ (π = π β suc π = suc π) |
8 | 7 | raleqdv 3312 |
. . . 4
β’ (π = π β (βπ β suc π(π΅βπ) β π« π β βπ β suc π(π΅βπ) β π« π)) |
9 | | iuneq1 4974 |
. . . . 5
β’ (π = π β βͺ
π β π (π΅βπ) = βͺ π β π (π΅βπ)) |
10 | | fveq2 6846 |
. . . . 5
β’ (π = π β (π΅βπ) = (π΅βπ)) |
11 | 9, 10 | breq12d 5122 |
. . . 4
β’ (π = π β (βͺ
π β π (π΅βπ) βΊ (π΅βπ) β βͺ
π β π (π΅βπ) βΊ (π΅βπ))) |
12 | 8, 11 | imbi12d 345 |
. . 3
β’ (π = π β ((βπ β suc π(π΅βπ) β π« π β βͺ
π β π (π΅βπ) βΊ (π΅βπ)) β (βπ β suc π(π΅βπ) β π« π β βͺ
π β π (π΅βπ) βΊ (π΅βπ)))) |
13 | | suceq 6387 |
. . . . 5
β’ (π = suc π β suc π = suc suc π) |
14 | 13 | raleqdv 3312 |
. . . 4
β’ (π = suc π β (βπ β suc π(π΅βπ) β π« π β βπ β suc suc π(π΅βπ) β π« π)) |
15 | | iuneq1 4974 |
. . . . 5
β’ (π = suc π β βͺ
π β π (π΅βπ) = βͺ π β suc π(π΅βπ)) |
16 | | fveq2 6846 |
. . . . 5
β’ (π = suc π β (π΅βπ) = (π΅βsuc π)) |
17 | 15, 16 | breq12d 5122 |
. . . 4
β’ (π = suc π β (βͺ
π β π (π΅βπ) βΊ (π΅βπ) β βͺ
π β suc π(π΅βπ) βΊ (π΅βsuc π))) |
18 | 14, 17 | imbi12d 345 |
. . 3
β’ (π = suc π β ((βπ β suc π(π΅βπ) β π« π β βͺ
π β π (π΅βπ) βΊ (π΅βπ)) β (βπ β suc suc π(π΅βπ) β π« π β βͺ
π β suc π(π΅βπ) βΊ (π΅βsuc π)))) |
19 | | 0iun 5027 |
. . . 4
β’ βͺ π β β
(π΅βπ) = β
|
20 | | 0ex 5268 |
. . . . . . 7
β’ β
β V |
21 | 20 | sucid 6403 |
. . . . . 6
β’ β
β suc β
|
22 | | fveq2 6846 |
. . . . . . . 8
β’ (π = β
β (π΅βπ) = (π΅ββ
)) |
23 | | pweq 4578 |
. . . . . . . 8
β’ (π = β
β π«
π = π«
β
) |
24 | 22, 23 | breq12d 5122 |
. . . . . . 7
β’ (π = β
β ((π΅βπ) β π« π β (π΅ββ
) β π«
β
)) |
25 | 24 | rspcv 3579 |
. . . . . 6
β’ (β
β suc β
β (βπ β suc β
(π΅βπ) β π« π β (π΅ββ
) β π«
β
)) |
26 | 21, 25 | ax-mp 5 |
. . . . 5
β’
(βπ β
suc β
(π΅βπ) β π« π β (π΅ββ
) β π«
β
) |
27 | 20 | canth2 9080 |
. . . . . 6
β’ β
βΊ π« β
|
28 | | ensym 8949 |
. . . . . 6
β’ ((π΅ββ
) β
π« β
β π« β
β (π΅ββ
)) |
29 | | sdomentr 9061 |
. . . . . 6
β’ ((β
βΊ π« β
β§ π« β
β (π΅ββ
)) β β
βΊ
(π΅ββ
)) |
30 | 27, 28, 29 | sylancr 588 |
. . . . 5
β’ ((π΅ββ
) β
π« β
β β
βΊ (π΅ββ
)) |
31 | 26, 30 | syl 17 |
. . . 4
β’
(βπ β
suc β
(π΅βπ) β π« π β β
βΊ (π΅ββ
)) |
32 | 19, 31 | eqbrtrid 5144 |
. . 3
β’
(βπ β
suc β
(π΅βπ) β π« π β βͺ π β β
(π΅βπ) βΊ (π΅ββ
)) |
33 | | sssucid 6401 |
. . . . . . . . 9
β’ suc π β suc suc π |
34 | | ssralv 4014 |
. . . . . . . . 9
β’ (suc
π β suc suc π β (βπ β suc suc π(π΅βπ) β π« π β βπ β suc π(π΅βπ) β π« π)) |
35 | 33, 34 | ax-mp 5 |
. . . . . . . 8
β’
(βπ β
suc suc π(π΅βπ) β π« π β βπ β suc π(π΅βπ) β π« π) |
36 | | pm2.27 42 |
. . . . . . . 8
β’
(βπ β
suc π(π΅βπ) β π« π β ((βπ β suc π(π΅βπ) β π« π β βͺ
π β π (π΅βπ) βΊ (π΅βπ)) β βͺ
π β π (π΅βπ) βΊ (π΅βπ))) |
37 | 35, 36 | syl 17 |
. . . . . . 7
β’
(βπ β
suc suc π(π΅βπ) β π« π β ((βπ β suc π(π΅βπ) β π« π β βͺ
π β π (π΅βπ) βΊ (π΅βπ)) β βͺ
π β π (π΅βπ) βΊ (π΅βπ))) |
38 | 37 | adantl 483 |
. . . . . 6
β’ ((π β Ο β§
βπ β suc suc
π(π΅βπ) β π« π) β ((βπ β suc π(π΅βπ) β π« π β βͺ
π β π (π΅βπ) βΊ (π΅βπ)) β βͺ
π β π (π΅βπ) βΊ (π΅βπ))) |
39 | | vex 3451 |
. . . . . . . . . . . . 13
β’ π β V |
40 | 39 | sucid 6403 |
. . . . . . . . . . . 12
β’ π β suc π |
41 | | elelsuc 6394 |
. . . . . . . . . . . 12
β’ (π β suc π β π β suc suc π) |
42 | | fveq2 6846 |
. . . . . . . . . . . . . 14
β’ (π = π β (π΅βπ) = (π΅βπ)) |
43 | | pweq 4578 |
. . . . . . . . . . . . . 14
β’ (π = π β π« π = π« π) |
44 | 42, 43 | breq12d 5122 |
. . . . . . . . . . . . 13
β’ (π = π β ((π΅βπ) β π« π β (π΅βπ) β π« π)) |
45 | 44 | rspcv 3579 |
. . . . . . . . . . . 12
β’ (π β suc suc π β (βπ β suc suc π(π΅βπ) β π« π β (π΅βπ) β π« π)) |
46 | 40, 41, 45 | mp2b 10 |
. . . . . . . . . . 11
β’
(βπ β
suc suc π(π΅βπ) β π« π β (π΅βπ) β π« π) |
47 | | djuen 10113 |
. . . . . . . . . . 11
β’ (((π΅βπ) β π« π β§ (π΅βπ) β π« π) β ((π΅βπ) β (π΅βπ)) β (π« π β π« π)) |
48 | 46, 46, 47 | syl2anc 585 |
. . . . . . . . . 10
β’
(βπ β
suc suc π(π΅βπ) β π« π β ((π΅βπ) β (π΅βπ)) β (π« π β π« π)) |
49 | | pwdju1 10134 |
. . . . . . . . . . 11
β’ (π β Ο β
(π« π β
π« π) β
π« (π β
1o)) |
50 | | nnord 7814 |
. . . . . . . . . . . . . 14
β’ (π β Ο β Ord π) |
51 | | ordirr 6339 |
. . . . . . . . . . . . . 14
β’ (Ord
π β Β¬ π β π) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β Ο β Β¬
π β π) |
53 | | dju1en 10115 |
. . . . . . . . . . . . 13
β’ ((π β Ο β§ Β¬
π β π) β (π β 1o) β suc π) |
54 | 52, 53 | mpdan 686 |
. . . . . . . . . . . 12
β’ (π β Ο β (π β 1o) β
suc π) |
55 | | pwen 9100 |
. . . . . . . . . . . 12
β’ ((π β 1o) β
suc π β π«
(π β 1o)
β π« suc π) |
56 | 54, 55 | syl 17 |
. . . . . . . . . . 11
β’ (π β Ο β π«
(π β 1o)
β π« suc π) |
57 | | entr 8952 |
. . . . . . . . . . 11
β’
(((π« π
β π« π)
β π« (π
β 1o) β§ π« (π β 1o) β π«
suc π) β (π«
π β π« π) β π« suc π) |
58 | 49, 56, 57 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β Ο β
(π« π β
π« π) β
π« suc π) |
59 | | entr 8952 |
. . . . . . . . . 10
β’ ((((π΅βπ) β (π΅βπ)) β (π« π β π« π) β§ (π« π β π« π) β π« suc π) β ((π΅βπ) β (π΅βπ)) β π« suc π) |
60 | 48, 58, 59 | syl2an 597 |
. . . . . . . . 9
β’
((βπ β
suc suc π(π΅βπ) β π« π β§ π β Ο) β ((π΅βπ) β (π΅βπ)) β π« suc π) |
61 | 39 | sucex 7745 |
. . . . . . . . . . . . 13
β’ suc π β V |
62 | 61 | sucid 6403 |
. . . . . . . . . . . 12
β’ suc π β suc suc π |
63 | | fveq2 6846 |
. . . . . . . . . . . . . 14
β’ (π = suc π β (π΅βπ) = (π΅βsuc π)) |
64 | | pweq 4578 |
. . . . . . . . . . . . . 14
β’ (π = suc π β π« π = π« suc π) |
65 | 63, 64 | breq12d 5122 |
. . . . . . . . . . . . 13
β’ (π = suc π β ((π΅βπ) β π« π β (π΅βsuc π) β π« suc π)) |
66 | 65 | rspcv 3579 |
. . . . . . . . . . . 12
β’ (suc
π β suc suc π β (βπ β suc suc π(π΅βπ) β π« π β (π΅βsuc π) β π« suc π)) |
67 | 62, 66 | ax-mp 5 |
. . . . . . . . . . 11
β’
(βπ β
suc suc π(π΅βπ) β π« π β (π΅βsuc π) β π« suc π) |
68 | 67 | ensymd 8951 |
. . . . . . . . . 10
β’
(βπ β
suc suc π(π΅βπ) β π« π β π« suc π β (π΅βsuc π)) |
69 | 68 | adantr 482 |
. . . . . . . . 9
β’
((βπ β
suc suc π(π΅βπ) β π« π β§ π β Ο) β π« suc π β (π΅βsuc π)) |
70 | | entr 8952 |
. . . . . . . . 9
β’ ((((π΅βπ) β (π΅βπ)) β π« suc π β§ π« suc π β (π΅βsuc π)) β ((π΅βπ) β (π΅βπ)) β (π΅βsuc π)) |
71 | 60, 69, 70 | syl2anc 585 |
. . . . . . . 8
β’
((βπ β
suc suc π(π΅βπ) β π« π β§ π β Ο) β ((π΅βπ) β (π΅βπ)) β (π΅βsuc π)) |
72 | 71 | ancoms 460 |
. . . . . . 7
β’ ((π β Ο β§
βπ β suc suc
π(π΅βπ) β π« π) β ((π΅βπ) β (π΅βπ)) β (π΅βsuc π)) |
73 | | nnfi 9117 |
. . . . . . . . . . . 12
β’ (π β Ο β π β Fin) |
74 | | pwfi 9128 |
. . . . . . . . . . . . 13
β’ (π β Fin β π«
π β
Fin) |
75 | | isfinite 9596 |
. . . . . . . . . . . . 13
β’
(π« π β
Fin β π« π
βΊ Ο) |
76 | 74, 75 | bitri 275 |
. . . . . . . . . . . 12
β’ (π β Fin β π«
π βΊ
Ο) |
77 | 73, 76 | sylib 217 |
. . . . . . . . . . 11
β’ (π β Ο β π«
π βΊ
Ο) |
78 | | ensdomtr 9063 |
. . . . . . . . . . 11
β’ (((π΅βπ) β π« π β§ π« π βΊ Ο) β (π΅βπ) βΊ Ο) |
79 | 46, 77, 78 | syl2an 597 |
. . . . . . . . . 10
β’
((βπ β
suc suc π(π΅βπ) β π« π β§ π β Ο) β (π΅βπ) βΊ Ο) |
80 | | isfinite 9596 |
. . . . . . . . . 10
β’ ((π΅βπ) β Fin β (π΅βπ) βΊ Ο) |
81 | 79, 80 | sylibr 233 |
. . . . . . . . 9
β’
((βπ β
suc suc π(π΅βπ) β π« π β§ π β Ο) β (π΅βπ) β Fin) |
82 | 81 | ancoms 460 |
. . . . . . . 8
β’ ((π β Ο β§
βπ β suc suc
π(π΅βπ) β π« π) β (π΅βπ) β Fin) |
83 | 39, 42 | iunsuc 6406 |
. . . . . . . . . . 11
β’ βͺ π β suc π(π΅βπ) = (βͺ
π β π (π΅βπ) βͺ (π΅βπ)) |
84 | | fvex 6859 |
. . . . . . . . . . . . 13
β’ (π΅βπ) β V |
85 | 39, 84 | iunex 7905 |
. . . . . . . . . . . 12
β’ βͺ π β π (π΅βπ) β V |
86 | | fvex 6859 |
. . . . . . . . . . . 12
β’ (π΅βπ) β V |
87 | | undjudom 10111 |
. . . . . . . . . . . 12
β’
((βͺ π β π (π΅βπ) β V β§ (π΅βπ) β V) β (βͺ π β π (π΅βπ) βͺ (π΅βπ)) βΌ (βͺ π β π (π΅βπ) β (π΅βπ))) |
88 | 85, 86, 87 | mp2an 691 |
. . . . . . . . . . 11
β’ (βͺ π β π (π΅βπ) βͺ (π΅βπ)) βΌ (βͺ π β π (π΅βπ) β (π΅βπ)) |
89 | 83, 88 | eqbrtri 5130 |
. . . . . . . . . 10
β’ βͺ π β suc π(π΅βπ) βΌ (βͺ π β π (π΅βπ) β (π΅βπ)) |
90 | | sdomtr 9065 |
. . . . . . . . . . . . . . . 16
β’
((βͺ π β π (π΅βπ) βΊ (π΅βπ) β§ (π΅βπ) βΊ Ο) β βͺ π β π (π΅βπ) βΊ Ο) |
91 | 80, 90 | sylan2b 595 |
. . . . . . . . . . . . . . 15
β’
((βͺ π β π (π΅βπ) βΊ (π΅βπ) β§ (π΅βπ) β Fin) β βͺ π β π (π΅βπ) βΊ Ο) |
92 | | isfinite 9596 |
. . . . . . . . . . . . . . 15
β’ (βͺ π β π (π΅βπ) β Fin β βͺ π β π (π΅βπ) βΊ Ο) |
93 | 91, 92 | sylibr 233 |
. . . . . . . . . . . . . 14
β’
((βͺ π β π (π΅βπ) βΊ (π΅βπ) β§ (π΅βπ) β Fin) β βͺ π β π (π΅βπ) β Fin) |
94 | | finnum 9892 |
. . . . . . . . . . . . . 14
β’ (βͺ π β π (π΅βπ) β Fin β βͺ π β π (π΅βπ) β dom card) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . 13
β’
((βͺ π β π (π΅βπ) βΊ (π΅βπ) β§ (π΅βπ) β Fin) β βͺ π β π (π΅βπ) β dom card) |
96 | | finnum 9892 |
. . . . . . . . . . . . . 14
β’ ((π΅βπ) β Fin β (π΅βπ) β dom card) |
97 | 96 | adantl 483 |
. . . . . . . . . . . . 13
β’
((βͺ π β π (π΅βπ) βΊ (π΅βπ) β§ (π΅βπ) β Fin) β (π΅βπ) β dom card) |
98 | | cardadju 10138 |
. . . . . . . . . . . . 13
β’
((βͺ π β π (π΅βπ) β dom card β§ (π΅βπ) β dom card) β (βͺ π β π (π΅βπ) β (π΅βπ)) β ((cardββͺ π β π (π΅βπ)) +o (cardβ(π΅βπ)))) |
99 | 95, 97, 98 | syl2anc 585 |
. . . . . . . . . . . 12
β’
((βͺ π β π (π΅βπ) βΊ (π΅βπ) β§ (π΅βπ) β Fin) β (βͺ π β π (π΅βπ) β (π΅βπ)) β ((cardββͺ π β π (π΅βπ)) +o (cardβ(π΅βπ)))) |
100 | | ficardom 9905 |
. . . . . . . . . . . . . . . 16
β’ (βͺ π β π (π΅βπ) β Fin β (cardββͺ π β π (π΅βπ)) β Ο) |
101 | 93, 100 | syl 17 |
. . . . . . . . . . . . . . 15
β’
((βͺ π β π (π΅βπ) βΊ (π΅βπ) β§ (π΅βπ) β Fin) β (cardββͺ π β π (π΅βπ)) β Ο) |
102 | | ficardom 9905 |
. . . . . . . . . . . . . . . 16
β’ ((π΅βπ) β Fin β (cardβ(π΅βπ)) β Ο) |
103 | 102 | adantl 483 |
. . . . . . . . . . . . . . 15
β’
((βͺ π β π (π΅βπ) βΊ (π΅βπ) β§ (π΅βπ) β Fin) β (cardβ(π΅βπ)) β Ο) |
104 | | cardid2 9897 |
. . . . . . . . . . . . . . . . . 18
β’ (βͺ π β π (π΅βπ) β dom card β (cardββͺ π β π (π΅βπ)) β βͺ π β π (π΅βπ)) |
105 | 93, 94, 104 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
β’
((βͺ π β π (π΅βπ) βΊ (π΅βπ) β§ (π΅βπ) β Fin) β (cardββͺ π β π (π΅βπ)) β βͺ π β π (π΅βπ)) |
106 | | simpl 484 |
. . . . . . . . . . . . . . . . 17
β’
((βͺ π β π (π΅βπ) βΊ (π΅βπ) β§ (π΅βπ) β Fin) β βͺ π β π (π΅βπ) βΊ (π΅βπ)) |
107 | | cardid2 9897 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΅βπ) β dom card β (cardβ(π΅βπ)) β (π΅βπ)) |
108 | | ensym 8949 |
. . . . . . . . . . . . . . . . . . 19
β’
((cardβ(π΅βπ)) β (π΅βπ) β (π΅βπ) β (cardβ(π΅βπ))) |
109 | 96, 107, 108 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΅βπ) β Fin β (π΅βπ) β (cardβ(π΅βπ))) |
110 | 109 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’
((βͺ π β π (π΅βπ) βΊ (π΅βπ) β§ (π΅βπ) β Fin) β (π΅βπ) β (cardβ(π΅βπ))) |
111 | | ensdomtr 9063 |
. . . . . . . . . . . . . . . . . 18
β’
(((cardββͺ π β π (π΅βπ)) β βͺ π β π (π΅βπ) β§ βͺ
π β π (π΅βπ) βΊ (π΅βπ)) β (cardββͺ π β π (π΅βπ)) βΊ (π΅βπ)) |
112 | | sdomentr 9061 |
. . . . . . . . . . . . . . . . . 18
β’
(((cardββͺ π β π (π΅βπ)) βΊ (π΅βπ) β§ (π΅βπ) β (cardβ(π΅βπ))) β (cardββͺ π β π (π΅βπ)) βΊ (cardβ(π΅βπ))) |
113 | 111, 112 | sylan 581 |
. . . . . . . . . . . . . . . . 17
β’
((((cardββͺ π β π (π΅βπ)) β βͺ π β π (π΅βπ) β§ βͺ
π β π (π΅βπ) βΊ (π΅βπ)) β§ (π΅βπ) β (cardβ(π΅βπ))) β (cardββͺ π β π (π΅βπ)) βΊ (cardβ(π΅βπ))) |
114 | 105, 106,
110, 113 | syl21anc 837 |
. . . . . . . . . . . . . . . 16
β’
((βͺ π β π (π΅βπ) βΊ (π΅βπ) β§ (π΅βπ) β Fin) β (cardββͺ π β π (π΅βπ)) βΊ (cardβ(π΅βπ))) |
115 | | cardon 9888 |
. . . . . . . . . . . . . . . . . 18
β’
(cardββͺ π β π (π΅βπ)) β On |
116 | | cardon 9888 |
. . . . . . . . . . . . . . . . . . 19
β’
(cardβ(π΅βπ)) β On |
117 | | onenon 9893 |
. . . . . . . . . . . . . . . . . . 19
β’
((cardβ(π΅βπ)) β On β (cardβ(π΅βπ)) β dom card) |
118 | 116, 117 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
β’
(cardβ(π΅βπ)) β dom card |
119 | | cardsdomel 9918 |
. . . . . . . . . . . . . . . . . 18
β’
(((cardββͺ π β π (π΅βπ)) β On β§ (cardβ(π΅βπ)) β dom card) β
((cardββͺ π β π (π΅βπ)) βΊ (cardβ(π΅βπ)) β (cardββͺ π β π (π΅βπ)) β (cardβ(cardβ(π΅βπ))))) |
120 | 115, 118,
119 | mp2an 691 |
. . . . . . . . . . . . . . . . 17
β’
((cardββͺ π β π (π΅βπ)) βΊ (cardβ(π΅βπ)) β (cardββͺ π β π (π΅βπ)) β (cardβ(cardβ(π΅βπ)))) |
121 | | cardidm 9903 |
. . . . . . . . . . . . . . . . . 18
β’
(cardβ(cardβ(π΅βπ))) = (cardβ(π΅βπ)) |
122 | 121 | eleq2i 2826 |
. . . . . . . . . . . . . . . . 17
β’
((cardββͺ π β π (π΅βπ)) β (cardβ(cardβ(π΅βπ))) β (cardββͺ π β π (π΅βπ)) β (cardβ(π΅βπ))) |
123 | 120, 122 | bitri 275 |
. . . . . . . . . . . . . . . 16
β’
((cardββͺ π β π (π΅βπ)) βΊ (cardβ(π΅βπ)) β (cardββͺ π β π (π΅βπ)) β (cardβ(π΅βπ))) |
124 | 114, 123 | sylib 217 |
. . . . . . . . . . . . . . 15
β’
((βͺ π β π (π΅βπ) βΊ (π΅βπ) β§ (π΅βπ) β Fin) β (cardββͺ π β π (π΅βπ)) β (cardβ(π΅βπ))) |
125 | | nnaordr 8571 |
. . . . . . . . . . . . . . . 16
β’
(((cardββͺ π β π (π΅βπ)) β Ο β§ (cardβ(π΅βπ)) β Ο β§ (cardβ(π΅βπ)) β Ο) β
((cardββͺ π β π (π΅βπ)) β (cardβ(π΅βπ)) β ((cardββͺ π β π (π΅βπ)) +o (cardβ(π΅βπ))) β ((cardβ(π΅βπ)) +o (cardβ(π΅βπ))))) |
126 | 125 | biimpa 478 |
. . . . . . . . . . . . . . 15
β’
((((cardββͺ π β π (π΅βπ)) β Ο β§ (cardβ(π΅βπ)) β Ο β§ (cardβ(π΅βπ)) β Ο) β§ (cardββͺ π β π (π΅βπ)) β (cardβ(π΅βπ))) β ((cardββͺ π β π (π΅βπ)) +o (cardβ(π΅βπ))) β ((cardβ(π΅βπ)) +o (cardβ(π΅βπ)))) |
127 | 101, 103,
103, 124, 126 | syl31anc 1374 |
. . . . . . . . . . . . . 14
β’
((βͺ π β π (π΅βπ) βΊ (π΅βπ) β§ (π΅βπ) β Fin) β ((cardββͺ π β π (π΅βπ)) +o (cardβ(π΅βπ))) β ((cardβ(π΅βπ)) +o (cardβ(π΅βπ)))) |
128 | | nnacl 8562 |
. . . . . . . . . . . . . . . . 17
β’
(((cardβ(π΅βπ)) β Ο β§ (cardβ(π΅βπ)) β Ο) β ((cardβ(π΅βπ)) +o (cardβ(π΅βπ))) β Ο) |
129 | 102, 102,
128 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((π΅βπ) β Fin β ((cardβ(π΅βπ)) +o (cardβ(π΅βπ))) β Ο) |
130 | | cardnn 9907 |
. . . . . . . . . . . . . . . 16
β’
(((cardβ(π΅βπ)) +o (cardβ(π΅βπ))) β Ο β
(cardβ((cardβ(π΅βπ)) +o (cardβ(π΅βπ)))) = ((cardβ(π΅βπ)) +o (cardβ(π΅βπ)))) |
131 | 129, 130 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π΅βπ) β Fin β
(cardβ((cardβ(π΅βπ)) +o (cardβ(π΅βπ)))) = ((cardβ(π΅βπ)) +o (cardβ(π΅βπ)))) |
132 | 131 | adantl 483 |
. . . . . . . . . . . . . 14
β’
((βͺ π β π (π΅βπ) βΊ (π΅βπ) β§ (π΅βπ) β Fin) β
(cardβ((cardβ(π΅βπ)) +o (cardβ(π΅βπ)))) = ((cardβ(π΅βπ)) +o (cardβ(π΅βπ)))) |
133 | 127, 132 | eleqtrrd 2837 |
. . . . . . . . . . . . 13
β’
((βͺ π β π (π΅βπ) βΊ (π΅βπ) β§ (π΅βπ) β Fin) β ((cardββͺ π β π (π΅βπ)) +o (cardβ(π΅βπ))) β (cardβ((cardβ(π΅βπ)) +o (cardβ(π΅βπ))))) |
134 | | cardsdomelir 9917 |
. . . . . . . . . . . . 13
β’
(((cardββͺ π β π (π΅βπ)) +o (cardβ(π΅βπ))) β (cardβ((cardβ(π΅βπ)) +o (cardβ(π΅βπ)))) β ((cardββͺ π β π (π΅βπ)) +o (cardβ(π΅βπ))) βΊ ((cardβ(π΅βπ)) +o (cardβ(π΅βπ)))) |
135 | 133, 134 | syl 17 |
. . . . . . . . . . . 12
β’
((βͺ π β π (π΅βπ) βΊ (π΅βπ) β§ (π΅βπ) β Fin) β ((cardββͺ π β π (π΅βπ)) +o (cardβ(π΅βπ))) βΊ ((cardβ(π΅βπ)) +o (cardβ(π΅βπ)))) |
136 | | ensdomtr 9063 |
. . . . . . . . . . . 12
β’
(((βͺ π β π (π΅βπ) β (π΅βπ)) β ((cardββͺ π β π (π΅βπ)) +o (cardβ(π΅βπ))) β§ ((cardββͺ π β π (π΅βπ)) +o (cardβ(π΅βπ))) βΊ ((cardβ(π΅βπ)) +o (cardβ(π΅βπ)))) β (βͺ π β π (π΅βπ) β (π΅βπ)) βΊ ((cardβ(π΅βπ)) +o (cardβ(π΅βπ)))) |
137 | 99, 135, 136 | syl2anc 585 |
. . . . . . . . . . 11
β’
((βͺ π β π (π΅βπ) βΊ (π΅βπ) β§ (π΅βπ) β Fin) β (βͺ π β π (π΅βπ) β (π΅βπ)) βΊ ((cardβ(π΅βπ)) +o (cardβ(π΅βπ)))) |
138 | | cardadju 10138 |
. . . . . . . . . . . . . 14
β’ (((π΅βπ) β dom card β§ (π΅βπ) β dom card) β ((π΅βπ) β (π΅βπ)) β ((cardβ(π΅βπ)) +o (cardβ(π΅βπ)))) |
139 | 96, 96, 138 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π΅βπ) β Fin β ((π΅βπ) β (π΅βπ)) β ((cardβ(π΅βπ)) +o (cardβ(π΅βπ)))) |
140 | 139 | ensymd 8951 |
. . . . . . . . . . . 12
β’ ((π΅βπ) β Fin β ((cardβ(π΅βπ)) +o (cardβ(π΅βπ))) β ((π΅βπ) β (π΅βπ))) |
141 | 140 | adantl 483 |
. . . . . . . . . . 11
β’
((βͺ π β π (π΅βπ) βΊ (π΅βπ) β§ (π΅βπ) β Fin) β ((cardβ(π΅βπ)) +o (cardβ(π΅βπ))) β ((π΅βπ) β (π΅βπ))) |
142 | | sdomentr 9061 |
. . . . . . . . . . 11
β’
(((βͺ π β π (π΅βπ) β (π΅βπ)) βΊ ((cardβ(π΅βπ)) +o (cardβ(π΅βπ))) β§ ((cardβ(π΅βπ)) +o (cardβ(π΅βπ))) β ((π΅βπ) β (π΅βπ))) β (βͺ π β π (π΅βπ) β (π΅βπ)) βΊ ((π΅βπ) β (π΅βπ))) |
143 | 137, 141,
142 | syl2anc 585 |
. . . . . . . . . 10
β’
((βͺ π β π (π΅βπ) βΊ (π΅βπ) β§ (π΅βπ) β Fin) β (βͺ π β π (π΅βπ) β (π΅βπ)) βΊ ((π΅βπ) β (π΅βπ))) |
144 | | domsdomtr 9062 |
. . . . . . . . . 10
β’
((βͺ π β suc π(π΅βπ) βΌ (βͺ π β π (π΅βπ) β (π΅βπ)) β§ (βͺ
π β π (π΅βπ) β (π΅βπ)) βΊ ((π΅βπ) β (π΅βπ))) β βͺ π β suc π(π΅βπ) βΊ ((π΅βπ) β (π΅βπ))) |
145 | 89, 143, 144 | sylancr 588 |
. . . . . . . . 9
β’
((βͺ π β π (π΅βπ) βΊ (π΅βπ) β§ (π΅βπ) β Fin) β βͺ π β suc π(π΅βπ) βΊ ((π΅βπ) β (π΅βπ))) |
146 | 145 | expcom 415 |
. . . . . . . 8
β’ ((π΅βπ) β Fin β (βͺ π β π (π΅βπ) βΊ (π΅βπ) β βͺ
π β suc π(π΅βπ) βΊ ((π΅βπ) β (π΅βπ)))) |
147 | 82, 146 | syl 17 |
. . . . . . 7
β’ ((π β Ο β§
βπ β suc suc
π(π΅βπ) β π« π) β (βͺ
π β π (π΅βπ) βΊ (π΅βπ) β βͺ
π β suc π(π΅βπ) βΊ ((π΅βπ) β (π΅βπ)))) |
148 | | sdomentr 9061 |
. . . . . . . 8
β’
((βͺ π β suc π(π΅βπ) βΊ ((π΅βπ) β (π΅βπ)) β§ ((π΅βπ) β (π΅βπ)) β (π΅βsuc π)) β βͺ
π β suc π(π΅βπ) βΊ (π΅βsuc π)) |
149 | 148 | expcom 415 |
. . . . . . 7
β’ (((π΅βπ) β (π΅βπ)) β (π΅βsuc π) β (βͺ
π β suc π(π΅βπ) βΊ ((π΅βπ) β (π΅βπ)) β βͺ
π β suc π(π΅βπ) βΊ (π΅βsuc π))) |
150 | 72, 147, 149 | sylsyld 61 |
. . . . . 6
β’ ((π β Ο β§
βπ β suc suc
π(π΅βπ) β π« π) β (βͺ
π β π (π΅βπ) βΊ (π΅βπ) β βͺ
π β suc π(π΅βπ) βΊ (π΅βsuc π))) |
151 | 38, 150 | syld 47 |
. . . . 5
β’ ((π β Ο β§
βπ β suc suc
π(π΅βπ) β π« π) β ((βπ β suc π(π΅βπ) β π« π β βͺ
π β π (π΅βπ) βΊ (π΅βπ)) β βͺ
π β suc π(π΅βπ) βΊ (π΅βsuc π))) |
152 | 151 | ex 414 |
. . . 4
β’ (π β Ο β
(βπ β suc suc
π(π΅βπ) β π« π β ((βπ β suc π(π΅βπ) β π« π β βͺ
π β π (π΅βπ) βΊ (π΅βπ)) β βͺ
π β suc π(π΅βπ) βΊ (π΅βsuc π)))) |
153 | 152 | com23 86 |
. . 3
β’ (π β Ο β
((βπ β suc
π(π΅βπ) β π« π β βͺ
π β π (π΅βπ) βΊ (π΅βπ)) β (βπ β suc suc π(π΅βπ) β π« π β βͺ
π β suc π(π΅βπ) βΊ (π΅βsuc π)))) |
154 | 6, 12, 18, 32, 153 | finds1 7842 |
. 2
β’ (π β Ο β
(βπ β suc π(π΅βπ) β π« π β βͺ
π β π (π΅βπ) βΊ (π΅βπ))) |
155 | 154 | imp 408 |
1
β’ ((π β Ο β§
βπ β suc π(π΅βπ) β π« π) β βͺ
π β π (π΅βπ) βΊ (π΅βπ)) |