Step | Hyp | Ref
| Expression |
1 | | r1elssi 9749 |
. . . . . 6
β’ (π΅ β βͺ (π
1 β On) β π΅ β βͺ (π
1 β On)) |
2 | 1 | sseld 3947 |
. . . . 5
β’ (π΅ β βͺ (π
1 β On) β (π΄ β π΅ β π΄ β βͺ
(π
1 β On))) |
3 | | rankidn 9766 |
. . . . 5
β’ (π΄ β βͺ (π
1 β On) β Β¬ π΄ β
(π
1β(rankβπ΄))) |
4 | 2, 3 | syl6 35 |
. . . 4
β’ (π΅ β βͺ (π
1 β On) β (π΄ β π΅ β Β¬ π΄ β
(π
1β(rankβπ΄)))) |
5 | 4 | imp 408 |
. . 3
β’ ((π΅ β βͺ (π
1 β On) β§ π΄ β π΅) β Β¬ π΄ β
(π
1β(rankβπ΄))) |
6 | | rankon 9739 |
. . . . 5
β’
(rankβπ΅)
β On |
7 | | rankon 9739 |
. . . . 5
β’
(rankβπ΄)
β On |
8 | | ontri1 6355 |
. . . . 5
β’
(((rankβπ΅)
β On β§ (rankβπ΄) β On) β ((rankβπ΅) β (rankβπ΄) β Β¬ (rankβπ΄) β (rankβπ΅))) |
9 | 6, 7, 8 | mp2an 691 |
. . . 4
β’
((rankβπ΅)
β (rankβπ΄)
β Β¬ (rankβπ΄)
β (rankβπ΅)) |
10 | | rankdmr1 9745 |
. . . . . 6
β’
(rankβπ΅)
β dom π
1 |
11 | | rankdmr1 9745 |
. . . . . 6
β’
(rankβπ΄)
β dom π
1 |
12 | | r1ord3g 9723 |
. . . . . 6
β’
(((rankβπ΅)
β dom π
1 β§ (rankβπ΄) β dom π
1) β
((rankβπ΅) β
(rankβπ΄) β
(π
1β(rankβπ΅)) β
(π
1β(rankβπ΄)))) |
13 | 10, 11, 12 | mp2an 691 |
. . . . 5
β’
((rankβπ΅)
β (rankβπ΄)
β (π
1β(rankβπ΅)) β
(π
1β(rankβπ΄))) |
14 | | r1rankidb 9748 |
. . . . . 6
β’ (π΅ β βͺ (π
1 β On) β π΅ β
(π
1β(rankβπ΅))) |
15 | 14 | sselda 3948 |
. . . . 5
β’ ((π΅ β βͺ (π
1 β On) β§ π΄ β π΅) β π΄ β
(π
1β(rankβπ΅))) |
16 | | ssel 3941 |
. . . . 5
β’
((π
1β(rankβπ΅)) β
(π
1β(rankβπ΄)) β (π΄ β
(π
1β(rankβπ΅)) β π΄ β
(π
1β(rankβπ΄)))) |
17 | 13, 15, 16 | syl2imc 41 |
. . . 4
β’ ((π΅ β βͺ (π
1 β On) β§ π΄ β π΅) β ((rankβπ΅) β (rankβπ΄) β π΄ β
(π
1β(rankβπ΄)))) |
18 | 9, 17 | biimtrrid 242 |
. . 3
β’ ((π΅ β βͺ (π
1 β On) β§ π΄ β π΅) β (Β¬ (rankβπ΄) β (rankβπ΅) β π΄ β
(π
1β(rankβπ΄)))) |
19 | 5, 18 | mt3d 148 |
. 2
β’ ((π΅ β βͺ (π
1 β On) β§ π΄ β π΅) β (rankβπ΄) β (rankβπ΅)) |
20 | 19 | ex 414 |
1
β’ (π΅ β βͺ (π
1 β On) β (π΄ β π΅ β (rankβπ΄) β (rankβπ΅))) |