Step | Hyp | Ref
| Expression |
1 | | unwf 9805 |
. . . . . . 7
β’ ((π΄ β βͺ (π
1 β On) β§ π΅ β βͺ (π
1 β On)) β (π΄ βͺ π΅) β βͺ
(π
1 β On)) |
2 | | rankval3b 9821 |
. . . . . . 7
β’ ((π΄ βͺ π΅) β βͺ
(π
1 β On) β (rankβ(π΄ βͺ π΅)) = β© {π¦ β On β£ βπ₯ β (π΄ βͺ π΅)(rankβπ₯) β π¦}) |
3 | 1, 2 | sylbi 216 |
. . . . . 6
β’ ((π΄ β βͺ (π
1 β On) β§ π΅ β βͺ (π
1 β On)) β
(rankβ(π΄ βͺ π΅)) = β© {π¦
β On β£ βπ₯
β (π΄ βͺ π΅)(rankβπ₯) β π¦}) |
4 | 3 | eleq2d 2820 |
. . . . 5
β’ ((π΄ β βͺ (π
1 β On) β§ π΅ β βͺ (π
1 β On)) β (π₯ β (rankβ(π΄ βͺ π΅)) β π₯ β β© {π¦ β On β£ βπ₯ β (π΄ βͺ π΅)(rankβπ₯) β π¦})) |
5 | | vex 3479 |
. . . . . 6
β’ π₯ β V |
6 | 5 | elintrab 4965 |
. . . . 5
β’ (π₯ β β© {π¦
β On β£ βπ₯
β (π΄ βͺ π΅)(rankβπ₯) β π¦} β βπ¦ β On (βπ₯ β (π΄ βͺ π΅)(rankβπ₯) β π¦ β π₯ β π¦)) |
7 | 4, 6 | bitrdi 287 |
. . . 4
β’ ((π΄ β βͺ (π
1 β On) β§ π΅ β βͺ (π
1 β On)) β (π₯ β (rankβ(π΄ βͺ π΅)) β βπ¦ β On (βπ₯ β (π΄ βͺ π΅)(rankβπ₯) β π¦ β π₯ β π¦))) |
8 | | elun 4149 |
. . . . . . 7
β’ (π₯ β (π΄ βͺ π΅) β (π₯ β π΄ β¨ π₯ β π΅)) |
9 | | rankelb 9819 |
. . . . . . . . 9
β’ (π΄ β βͺ (π
1 β On) β (π₯ β π΄ β (rankβπ₯) β (rankβπ΄))) |
10 | | elun1 4177 |
. . . . . . . . 9
β’
((rankβπ₯)
β (rankβπ΄)
β (rankβπ₯)
β ((rankβπ΄)
βͺ (rankβπ΅))) |
11 | 9, 10 | syl6 35 |
. . . . . . . 8
β’ (π΄ β βͺ (π
1 β On) β (π₯ β π΄ β (rankβπ₯) β ((rankβπ΄) βͺ (rankβπ΅)))) |
12 | | rankelb 9819 |
. . . . . . . . 9
β’ (π΅ β βͺ (π
1 β On) β (π₯ β π΅ β (rankβπ₯) β (rankβπ΅))) |
13 | | elun2 4178 |
. . . . . . . . 9
β’
((rankβπ₯)
β (rankβπ΅)
β (rankβπ₯)
β ((rankβπ΄)
βͺ (rankβπ΅))) |
14 | 12, 13 | syl6 35 |
. . . . . . . 8
β’ (π΅ β βͺ (π
1 β On) β (π₯ β π΅ β (rankβπ₯) β ((rankβπ΄) βͺ (rankβπ΅)))) |
15 | 11, 14 | jaao 954 |
. . . . . . 7
β’ ((π΄ β βͺ (π
1 β On) β§ π΅ β βͺ (π
1 β On)) β ((π₯ β π΄ β¨ π₯ β π΅) β (rankβπ₯) β ((rankβπ΄) βͺ (rankβπ΅)))) |
16 | 8, 15 | biimtrid 241 |
. . . . . 6
β’ ((π΄ β βͺ (π
1 β On) β§ π΅ β βͺ (π
1 β On)) β (π₯ β (π΄ βͺ π΅) β (rankβπ₯) β ((rankβπ΄) βͺ (rankβπ΅)))) |
17 | 16 | ralrimiv 3146 |
. . . . 5
β’ ((π΄ β βͺ (π
1 β On) β§ π΅ β βͺ (π
1 β On)) β βπ₯ β (π΄ βͺ π΅)(rankβπ₯) β ((rankβπ΄) βͺ (rankβπ΅))) |
18 | | rankon 9790 |
. . . . . . 7
β’
(rankβπ΄)
β On |
19 | | rankon 9790 |
. . . . . . 7
β’
(rankβπ΅)
β On |
20 | 18, 19 | onun2i 6487 |
. . . . . 6
β’
((rankβπ΄)
βͺ (rankβπ΅))
β On |
21 | | eleq2 2823 |
. . . . . . . . 9
β’ (π¦ = ((rankβπ΄) βͺ (rankβπ΅)) β ((rankβπ₯) β π¦ β (rankβπ₯) β ((rankβπ΄) βͺ (rankβπ΅)))) |
22 | 21 | ralbidv 3178 |
. . . . . . . 8
β’ (π¦ = ((rankβπ΄) βͺ (rankβπ΅)) β (βπ₯ β (π΄ βͺ π΅)(rankβπ₯) β π¦ β βπ₯ β (π΄ βͺ π΅)(rankβπ₯) β ((rankβπ΄) βͺ (rankβπ΅)))) |
23 | | eleq2 2823 |
. . . . . . . 8
β’ (π¦ = ((rankβπ΄) βͺ (rankβπ΅)) β (π₯ β π¦ β π₯ β ((rankβπ΄) βͺ (rankβπ΅)))) |
24 | 22, 23 | imbi12d 345 |
. . . . . . 7
β’ (π¦ = ((rankβπ΄) βͺ (rankβπ΅)) β ((βπ₯ β (π΄ βͺ π΅)(rankβπ₯) β π¦ β π₯ β π¦) β (βπ₯ β (π΄ βͺ π΅)(rankβπ₯) β ((rankβπ΄) βͺ (rankβπ΅)) β π₯ β ((rankβπ΄) βͺ (rankβπ΅))))) |
25 | 24 | rspcv 3609 |
. . . . . 6
β’
(((rankβπ΄)
βͺ (rankβπ΅))
β On β (βπ¦
β On (βπ₯ β
(π΄ βͺ π΅)(rankβπ₯) β π¦ β π₯ β π¦) β (βπ₯ β (π΄ βͺ π΅)(rankβπ₯) β ((rankβπ΄) βͺ (rankβπ΅)) β π₯ β ((rankβπ΄) βͺ (rankβπ΅))))) |
26 | 20, 25 | ax-mp 5 |
. . . . 5
β’
(βπ¦ β On
(βπ₯ β (π΄ βͺ π΅)(rankβπ₯) β π¦ β π₯ β π¦) β (βπ₯ β (π΄ βͺ π΅)(rankβπ₯) β ((rankβπ΄) βͺ (rankβπ΅)) β π₯ β ((rankβπ΄) βͺ (rankβπ΅)))) |
27 | 17, 26 | syl5com 31 |
. . . 4
β’ ((π΄ β βͺ (π
1 β On) β§ π΅ β βͺ (π
1 β On)) β
(βπ¦ β On
(βπ₯ β (π΄ βͺ π΅)(rankβπ₯) β π¦ β π₯ β π¦) β π₯ β ((rankβπ΄) βͺ (rankβπ΅)))) |
28 | 7, 27 | sylbid 239 |
. . 3
β’ ((π΄ β βͺ (π
1 β On) β§ π΅ β βͺ (π
1 β On)) β (π₯ β (rankβ(π΄ βͺ π΅)) β π₯ β ((rankβπ΄) βͺ (rankβπ΅)))) |
29 | 28 | ssrdv 3989 |
. 2
β’ ((π΄ β βͺ (π
1 β On) β§ π΅ β βͺ (π
1 β On)) β
(rankβ(π΄ βͺ π΅)) β ((rankβπ΄) βͺ (rankβπ΅))) |
30 | | ssun1 4173 |
. . . . 5
β’ π΄ β (π΄ βͺ π΅) |
31 | | rankssb 9843 |
. . . . 5
β’ ((π΄ βͺ π΅) β βͺ
(π
1 β On) β (π΄ β (π΄ βͺ π΅) β (rankβπ΄) β (rankβ(π΄ βͺ π΅)))) |
32 | 30, 31 | mpi 20 |
. . . 4
β’ ((π΄ βͺ π΅) β βͺ
(π
1 β On) β (rankβπ΄) β (rankβ(π΄ βͺ π΅))) |
33 | | ssun2 4174 |
. . . . 5
β’ π΅ β (π΄ βͺ π΅) |
34 | | rankssb 9843 |
. . . . 5
β’ ((π΄ βͺ π΅) β βͺ
(π
1 β On) β (π΅ β (π΄ βͺ π΅) β (rankβπ΅) β (rankβ(π΄ βͺ π΅)))) |
35 | 33, 34 | mpi 20 |
. . . 4
β’ ((π΄ βͺ π΅) β βͺ
(π
1 β On) β (rankβπ΅) β (rankβ(π΄ βͺ π΅))) |
36 | 32, 35 | unssd 4187 |
. . 3
β’ ((π΄ βͺ π΅) β βͺ
(π
1 β On) β ((rankβπ΄) βͺ (rankβπ΅)) β (rankβ(π΄ βͺ π΅))) |
37 | 1, 36 | sylbi 216 |
. 2
β’ ((π΄ β βͺ (π
1 β On) β§ π΅ β βͺ (π
1 β On)) β
((rankβπ΄) βͺ
(rankβπ΅)) β
(rankβ(π΄ βͺ π΅))) |
38 | 29, 37 | eqssd 4000 |
1
β’ ((π΄ β βͺ (π
1 β On) β§ π΅ β βͺ (π
1 β On)) β
(rankβ(π΄ βͺ π΅)) = ((rankβπ΄) βͺ (rankβπ΅))) |