Step | Hyp | Ref
| Expression |
1 | | r1elssi 9799 |
. . . . . 6
β’ (π΅ β βͺ (π
1 β On) β π΅ β βͺ (π
1 β On)) |
2 | 1 | sseld 3981 |
. . . . 5
β’ (π΅ β βͺ (π
1 β On) β (π΄ β π΅ β π΄ β βͺ
(π
1 β On))) |
3 | | rankidn 9816 |
. . . . 5
β’ (π΄ β βͺ (π
1 β On) β Β¬ π΄ β
(π
1β(rankβπ΄))) |
4 | 2, 3 | syl6 35 |
. . . 4
β’ (π΅ β βͺ (π
1 β On) β (π΄ β π΅ β Β¬ π΄ β
(π
1β(rankβπ΄)))) |
5 | 4 | imp 407 |
. . 3
β’ ((π΅ β βͺ (π
1 β On) β§ π΄ β π΅) β Β¬ π΄ β
(π
1β(rankβπ΄))) |
6 | | rankon 9789 |
. . . . 5
β’
(rankβπ΅)
β On |
7 | | rankon 9789 |
. . . . 5
β’
(rankβπ΄)
β On |
8 | | ontri1 6398 |
. . . . 5
β’
(((rankβπ΅)
β On β§ (rankβπ΄) β On) β ((rankβπ΅) β (rankβπ΄) β Β¬ (rankβπ΄) β (rankβπ΅))) |
9 | 6, 7, 8 | mp2an 690 |
. . . 4
β’
((rankβπ΅)
β (rankβπ΄)
β Β¬ (rankβπ΄)
β (rankβπ΅)) |
10 | | rankdmr1 9795 |
. . . . . 6
β’
(rankβπ΅)
β dom π
1 |
11 | | rankdmr1 9795 |
. . . . . 6
β’
(rankβπ΄)
β dom π
1 |
12 | | r1ord3g 9773 |
. . . . . 6
β’
(((rankβπ΅)
β dom π
1 β§ (rankβπ΄) β dom π
1) β
((rankβπ΅) β
(rankβπ΄) β
(π
1β(rankβπ΅)) β
(π
1β(rankβπ΄)))) |
13 | 10, 11, 12 | mp2an 690 |
. . . . 5
β’
((rankβπ΅)
β (rankβπ΄)
β (π
1β(rankβπ΅)) β
(π
1β(rankβπ΄))) |
14 | | r1rankidb 9798 |
. . . . . 6
β’ (π΅ β βͺ (π
1 β On) β π΅ β
(π
1β(rankβπ΅))) |
15 | 14 | sselda 3982 |
. . . . 5
β’ ((π΅ β βͺ (π
1 β On) β§ π΄ β π΅) β π΄ β
(π
1β(rankβπ΅))) |
16 | | ssel 3975 |
. . . . 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 413 |
1
β’ (π΅ β βͺ (π
1 β On) β (π΄ β π΅ β (rankβπ΄) β (rankβπ΅))) |