Step | Hyp | Ref
| Expression |
1 | | snwf 9750 |
. . 3
β’ (π΅ β βͺ (π
1 β On) β {π΅} β βͺ (π
1 β On)) |
2 | | df-altop 34589 |
. . . . . 6
β’
βͺπ΄, π΅β« = {{π΄}, {π΄, {π΅}}} |
3 | 2 | fveq2i 6846 |
. . . . 5
β’
(rankββͺπ΄, π΅β«) = (rankβ{{π΄}, {π΄, {π΅}}}) |
4 | | snwf 9750 |
. . . . . . 7
β’ (π΄ β βͺ (π
1 β On) β {π΄} β βͺ (π
1 β On)) |
5 | 4 | adantr 482 |
. . . . . 6
β’ ((π΄ β βͺ (π
1 β On) β§ {π΅} β βͺ (π
1 β On)) β {π΄} β βͺ (π
1 β On)) |
6 | | prwf 9752 |
. . . . . 6
β’ ((π΄ β βͺ (π
1 β On) β§ {π΅} β βͺ (π
1 β On)) β {π΄, {π΅}} β βͺ
(π
1 β On)) |
7 | | rankprb 9792 |
. . . . . 6
β’ (({π΄} β βͺ (π
1 β On) β§ {π΄, {π΅}} β βͺ
(π
1 β On)) β (rankβ{{π΄}, {π΄, {π΅}}}) = suc ((rankβ{π΄}) βͺ (rankβ{π΄, {π΅}}))) |
8 | 5, 6, 7 | syl2anc 585 |
. . . . 5
β’ ((π΄ β βͺ (π
1 β On) β§ {π΅} β βͺ (π
1 β On)) β
(rankβ{{π΄}, {π΄, {π΅}}}) = suc ((rankβ{π΄}) βͺ (rankβ{π΄, {π΅}}))) |
9 | 3, 8 | eqtrid 2785 |
. . . 4
β’ ((π΄ β βͺ (π
1 β On) β§ {π΅} β βͺ (π
1 β On)) β
(rankββͺπ΄,
π΅β«) = suc
((rankβ{π΄}) βͺ
(rankβ{π΄, {π΅}}))) |
10 | | snsspr1 4775 |
. . . . . . . 8
β’ {π΄} β {π΄, {π΅}} |
11 | | ssequn1 4141 |
. . . . . . . 8
β’ ({π΄} β {π΄, {π΅}} β ({π΄} βͺ {π΄, {π΅}}) = {π΄, {π΅}}) |
12 | 10, 11 | mpbi 229 |
. . . . . . 7
β’ ({π΄} βͺ {π΄, {π΅}}) = {π΄, {π΅}} |
13 | 12 | fveq2i 6846 |
. . . . . 6
β’
(rankβ({π΄}
βͺ {π΄, {π΅}})) = (rankβ{π΄, {π΅}}) |
14 | | rankunb 9791 |
. . . . . . 7
β’ (({π΄} β βͺ (π
1 β On) β§ {π΄, {π΅}} β βͺ
(π
1 β On)) β (rankβ({π΄} βͺ {π΄, {π΅}})) = ((rankβ{π΄}) βͺ (rankβ{π΄, {π΅}}))) |
15 | 5, 6, 14 | syl2anc 585 |
. . . . . 6
β’ ((π΄ β βͺ (π
1 β On) β§ {π΅} β βͺ (π
1 β On)) β
(rankβ({π΄} βͺ
{π΄, {π΅}})) = ((rankβ{π΄}) βͺ (rankβ{π΄, {π΅}}))) |
16 | | rankprb 9792 |
. . . . . 6
β’ ((π΄ β βͺ (π
1 β On) β§ {π΅} β βͺ (π
1 β On)) β
(rankβ{π΄, {π΅}}) = suc ((rankβπ΄) βͺ (rankβ{π΅}))) |
17 | 13, 15, 16 | 3eqtr3a 2797 |
. . . . 5
β’ ((π΄ β βͺ (π
1 β On) β§ {π΅} β βͺ (π
1 β On)) β
((rankβ{π΄}) βͺ
(rankβ{π΄, {π΅}})) = suc ((rankβπ΄) βͺ (rankβ{π΅}))) |
18 | | suceq 6384 |
. . . . 5
β’
(((rankβ{π΄})
βͺ (rankβ{π΄,
{π΅}})) = suc
((rankβπ΄) βͺ
(rankβ{π΅})) β
suc ((rankβ{π΄}) βͺ
(rankβ{π΄, {π΅}})) = suc suc
((rankβπ΄) βͺ
(rankβ{π΅}))) |
19 | 17, 18 | syl 17 |
. . . 4
β’ ((π΄ β βͺ (π
1 β On) β§ {π΅} β βͺ (π
1 β On)) β suc
((rankβ{π΄}) βͺ
(rankβ{π΄, {π΅}})) = suc suc
((rankβπ΄) βͺ
(rankβ{π΅}))) |
20 | 9, 19 | eqtrd 2773 |
. . 3
β’ ((π΄ β βͺ (π
1 β On) β§ {π΅} β βͺ (π
1 β On)) β
(rankββͺπ΄,
π΅β«) = suc suc
((rankβπ΄) βͺ
(rankβ{π΅}))) |
21 | 1, 20 | sylan2 594 |
. 2
β’ ((π΄ β βͺ (π
1 β On) β§ π΅ β βͺ (π
1 β On)) β
(rankββͺπ΄,
π΅β«) = suc suc
((rankβπ΄) βͺ
(rankβ{π΅}))) |
22 | | ranksnb 9768 |
. . . . 5
β’ (π΅ β βͺ (π
1 β On) β
(rankβ{π΅}) = suc
(rankβπ΅)) |
23 | 22 | uneq2d 4124 |
. . . 4
β’ (π΅ β βͺ (π
1 β On) β
((rankβπ΄) βͺ
(rankβ{π΅})) =
((rankβπ΄) βͺ suc
(rankβπ΅))) |
24 | | suceq 6384 |
. . . 4
β’
(((rankβπ΄)
βͺ (rankβ{π΅})) =
((rankβπ΄) βͺ suc
(rankβπ΅)) β suc
((rankβπ΄) βͺ
(rankβ{π΅})) = suc
((rankβπ΄) βͺ suc
(rankβπ΅))) |
25 | | suceq 6384 |
. . . 4
β’ (suc
((rankβπ΄) βͺ
(rankβ{π΅})) = suc
((rankβπ΄) βͺ suc
(rankβπ΅)) β suc
suc ((rankβπ΄) βͺ
(rankβ{π΅})) = suc suc
((rankβπ΄) βͺ suc
(rankβπ΅))) |
26 | 23, 24, 25 | 3syl 18 |
. . 3
β’ (π΅ β βͺ (π
1 β On) β suc suc
((rankβπ΄) βͺ
(rankβ{π΅})) = suc suc
((rankβπ΄) βͺ suc
(rankβπ΅))) |
27 | 26 | adantl 483 |
. 2
β’ ((π΄ β βͺ (π
1 β On) β§ π΅ β βͺ (π
1 β On)) β suc suc
((rankβπ΄) βͺ
(rankβ{π΅})) = suc suc
((rankβπ΄) βͺ suc
(rankβπ΅))) |
28 | 21, 27 | eqtrd 2773 |
1
β’ ((π΄ β βͺ (π
1 β On) β§ π΅ β βͺ (π
1 β On)) β
(rankββͺπ΄,
π΅β«) = suc suc
((rankβπ΄) βͺ suc
(rankβπ΅))) |