Step | Hyp | Ref
| Expression |
1 | | mapsspw 8874 |
. . 3
β’ (π΄ βm π΅) β π« (π΅ Γ π΄) |
2 | | rankxpl.2 |
. . . . . 6
β’ π΅ β V |
3 | | rankxpl.1 |
. . . . . 6
β’ π΄ β V |
4 | 2, 3 | xpex 7737 |
. . . . 5
β’ (π΅ Γ π΄) β V |
5 | 4 | pwex 5371 |
. . . 4
β’ π«
(π΅ Γ π΄) β V |
6 | 5 | rankss 9846 |
. . 3
β’ ((π΄ βm π΅) β π« (π΅ Γ π΄) β (rankβ(π΄ βm π΅)) β (rankβπ« (π΅ Γ π΄))) |
7 | 1, 6 | ax-mp 5 |
. 2
β’
(rankβ(π΄
βm π΅))
β (rankβπ« (π΅ Γ π΄)) |
8 | 4 | rankpw 9840 |
. . 3
β’
(rankβπ« (π΅ Γ π΄)) = suc (rankβ(π΅ Γ π΄)) |
9 | 2, 3 | rankxpu 9873 |
. . . . 5
β’
(rankβ(π΅
Γ π΄)) β suc suc
(rankβ(π΅ βͺ π΄)) |
10 | | uncom 4148 |
. . . . . . . 8
β’ (π΅ βͺ π΄) = (π΄ βͺ π΅) |
11 | 10 | fveq2i 6888 |
. . . . . . 7
β’
(rankβ(π΅ βͺ
π΄)) = (rankβ(π΄ βͺ π΅)) |
12 | | suceq 6424 |
. . . . . . 7
β’
((rankβ(π΅
βͺ π΄)) =
(rankβ(π΄ βͺ π΅)) β suc (rankβ(π΅ βͺ π΄)) = suc (rankβ(π΄ βͺ π΅))) |
13 | 11, 12 | ax-mp 5 |
. . . . . 6
β’ suc
(rankβ(π΅ βͺ π΄)) = suc (rankβ(π΄ βͺ π΅)) |
14 | | suceq 6424 |
. . . . . 6
β’ (suc
(rankβ(π΅ βͺ π΄)) = suc (rankβ(π΄ βͺ π΅)) β suc suc (rankβ(π΅ βͺ π΄)) = suc suc (rankβ(π΄ βͺ π΅))) |
15 | 13, 14 | ax-mp 5 |
. . . . 5
β’ suc suc
(rankβ(π΅ βͺ π΄)) = suc suc (rankβ(π΄ βͺ π΅)) |
16 | 9, 15 | sseqtri 4013 |
. . . 4
β’
(rankβ(π΅
Γ π΄)) β suc suc
(rankβ(π΄ βͺ π΅)) |
17 | | rankon 9792 |
. . . . . 6
β’
(rankβ(π΅
Γ π΄)) β
On |
18 | 17 | onordi 6469 |
. . . . 5
β’ Ord
(rankβ(π΅ Γ
π΄)) |
19 | | rankon 9792 |
. . . . . . . 8
β’
(rankβ(π΄ βͺ
π΅)) β
On |
20 | 19 | onsuci 7824 |
. . . . . . 7
β’ suc
(rankβ(π΄ βͺ π΅)) β On |
21 | 20 | onsuci 7824 |
. . . . . 6
β’ suc suc
(rankβ(π΄ βͺ π΅)) β On |
22 | 21 | onordi 6469 |
. . . . 5
β’ Ord suc
suc (rankβ(π΄ βͺ
π΅)) |
23 | | ordsucsssuc 7808 |
. . . . 5
β’ ((Ord
(rankβ(π΅ Γ
π΄)) β§ Ord suc suc
(rankβ(π΄ βͺ π΅))) β ((rankβ(π΅ Γ π΄)) β suc suc (rankβ(π΄ βͺ π΅)) β suc (rankβ(π΅ Γ π΄)) β suc suc suc (rankβ(π΄ βͺ π΅)))) |
24 | 18, 22, 23 | mp2an 689 |
. . . 4
β’
((rankβ(π΅
Γ π΄)) β suc suc
(rankβ(π΄ βͺ π΅)) β suc (rankβ(π΅ Γ π΄)) β suc suc suc (rankβ(π΄ βͺ π΅))) |
25 | 16, 24 | mpbi 229 |
. . 3
β’ suc
(rankβ(π΅ Γ
π΄)) β suc suc suc
(rankβ(π΄ βͺ π΅)) |
26 | 8, 25 | eqsstri 4011 |
. 2
β’
(rankβπ« (π΅ Γ π΄)) β suc suc suc (rankβ(π΄ βͺ π΅)) |
27 | 7, 26 | sstri 3986 |
1
β’
(rankβ(π΄
βm π΅))
β suc suc suc (rankβ(π΄ βͺ π΅)) |