Step | Hyp | Ref
| Expression |
1 | | rankon 9739 |
. . . . . . . . . 10
β’
(rankβπ΄)
β On |
2 | | simprl 770 |
. . . . . . . . . 10
β’ ((π΄ β βͺ (π
1 β On) β§ (π₯ β On β§ βπ¦ β π΄ (rankβπ¦) β π₯)) β π₯ β On) |
3 | | ontri1 6355 |
. . . . . . . . . 10
β’
(((rankβπ΄)
β On β§ π₯ β
On) β ((rankβπ΄)
β π₯ β Β¬
π₯ β (rankβπ΄))) |
4 | 1, 2, 3 | sylancr 588 |
. . . . . . . . 9
β’ ((π΄ β βͺ (π
1 β On) β§ (π₯ β On β§ βπ¦ β π΄ (rankβπ¦) β π₯)) β ((rankβπ΄) β π₯ β Β¬ π₯ β (rankβπ΄))) |
5 | 4 | con2bid 355 |
. . . . . . . 8
β’ ((π΄ β βͺ (π
1 β On) β§ (π₯ β On β§ βπ¦ β π΄ (rankβπ¦) β π₯)) β (π₯ β (rankβπ΄) β Β¬ (rankβπ΄) β π₯)) |
6 | | r1elssi 9749 |
. . . . . . . . . . . . . . . . . 18
β’ (π΄ β βͺ (π
1 β On) β π΄ β βͺ (π
1 β On)) |
7 | 6 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β βͺ (π
1 β On) β§ π₯ β (rankβπ΄)) β π΄ β βͺ
(π
1 β On)) |
8 | 7 | sselda 3948 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β βͺ (π
1 β On) β§ π₯ β (rankβπ΄)) β§ π¦ β π΄) β π¦ β βͺ
(π
1 β On)) |
9 | | rankdmr1 9745 |
. . . . . . . . . . . . . . . . . 18
β’
(rankβπ΄)
β dom π
1 |
10 | | r1funlim 9710 |
. . . . . . . . . . . . . . . . . . . 20
β’ (Fun
π
1 β§ Lim dom π
1) |
11 | 10 | simpri 487 |
. . . . . . . . . . . . . . . . . . 19
β’ Lim dom
π
1 |
12 | | limord 6381 |
. . . . . . . . . . . . . . . . . . 19
β’ (Lim dom
π
1 β Ord dom π
1) |
13 | | ordtr1 6364 |
. . . . . . . . . . . . . . . . . . 19
β’ (Ord dom
π
1 β ((π₯ β (rankβπ΄) β§ (rankβπ΄) β dom π
1) β
π₯ β dom
π
1)) |
14 | 11, 12, 13 | mp2b 10 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β (rankβπ΄) β§ (rankβπ΄) β dom
π
1) β π₯ β dom
π
1) |
15 | 9, 14 | mpan2 690 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β (rankβπ΄) β π₯ β dom
π
1) |
16 | 15 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β βͺ (π
1 β On) β§ π₯ β (rankβπ΄)) β§ π¦ β π΄) β π₯ β dom
π
1) |
17 | | rankr1ag 9746 |
. . . . . . . . . . . . . . . 16
β’ ((π¦ β βͺ (π
1 β On) β§ π₯ β dom
π
1) β (π¦ β (π
1βπ₯) β (rankβπ¦) β π₯)) |
18 | 8, 16, 17 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β βͺ (π
1 β On) β§ π₯ β (rankβπ΄)) β§ π¦ β π΄) β (π¦ β (π
1βπ₯) β (rankβπ¦) β π₯)) |
19 | 18 | ralbidva 3169 |
. . . . . . . . . . . . . 14
β’ ((π΄ β βͺ (π
1 β On) β§ π₯ β (rankβπ΄)) β (βπ¦ β π΄ π¦ β (π
1βπ₯) β βπ¦ β π΄ (rankβπ¦) β π₯)) |
20 | 19 | biimpar 479 |
. . . . . . . . . . . . 13
β’ (((π΄ β βͺ (π
1 β On) β§ π₯ β (rankβπ΄)) β§ βπ¦ β π΄ (rankβπ¦) β π₯) β βπ¦ β π΄ π¦ β (π
1βπ₯)) |
21 | 20 | an32s 651 |
. . . . . . . . . . . 12
β’ (((π΄ β βͺ (π
1 β On) β§ βπ¦ β π΄ (rankβπ¦) β π₯) β§ π₯ β (rankβπ΄)) β βπ¦ β π΄ π¦ β (π
1βπ₯)) |
22 | | dfss3 3936 |
. . . . . . . . . . . 12
β’ (π΄ β
(π
1βπ₯) β βπ¦ β π΄ π¦ β (π
1βπ₯)) |
23 | 21, 22 | sylibr 233 |
. . . . . . . . . . 11
β’ (((π΄ β βͺ (π
1 β On) β§ βπ¦ β π΄ (rankβπ¦) β π₯) β§ π₯ β (rankβπ΄)) β π΄ β (π
1βπ₯)) |
24 | | simpll 766 |
. . . . . . . . . . . 12
β’ (((π΄ β βͺ (π
1 β On) β§ βπ¦ β π΄ (rankβπ¦) β π₯) β§ π₯ β (rankβπ΄)) β π΄ β βͺ
(π
1 β On)) |
25 | 15 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π΄ β βͺ (π
1 β On) β§ βπ¦ β π΄ (rankβπ¦) β π₯) β§ π₯ β (rankβπ΄)) β π₯ β dom
π
1) |
26 | | rankr1bg 9747 |
. . . . . . . . . . . 12
β’ ((π΄ β βͺ (π
1 β On) β§ π₯ β dom
π
1) β (π΄ β (π
1βπ₯) β (rankβπ΄) β π₯)) |
27 | 24, 25, 26 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π΄ β βͺ (π
1 β On) β§ βπ¦ β π΄ (rankβπ¦) β π₯) β§ π₯ β (rankβπ΄)) β (π΄ β (π
1βπ₯) β (rankβπ΄) β π₯)) |
28 | 23, 27 | mpbid 231 |
. . . . . . . . . 10
β’ (((π΄ β βͺ (π
1 β On) β§ βπ¦ β π΄ (rankβπ¦) β π₯) β§ π₯ β (rankβπ΄)) β (rankβπ΄) β π₯) |
29 | 28 | ex 414 |
. . . . . . . . 9
β’ ((π΄ β βͺ (π
1 β On) β§ βπ¦ β π΄ (rankβπ¦) β π₯) β (π₯ β (rankβπ΄) β (rankβπ΄) β π₯)) |
30 | 29 | adantrl 715 |
. . . . . . . 8
β’ ((π΄ β βͺ (π
1 β On) β§ (π₯ β On β§ βπ¦ β π΄ (rankβπ¦) β π₯)) β (π₯ β (rankβπ΄) β (rankβπ΄) β π₯)) |
31 | 5, 30 | sylbird 260 |
. . . . . . 7
β’ ((π΄ β βͺ (π
1 β On) β§ (π₯ β On β§ βπ¦ β π΄ (rankβπ¦) β π₯)) β (Β¬ (rankβπ΄) β π₯ β (rankβπ΄) β π₯)) |
32 | 31 | pm2.18d 127 |
. . . . . 6
β’ ((π΄ β βͺ (π
1 β On) β§ (π₯ β On β§ βπ¦ β π΄ (rankβπ¦) β π₯)) β (rankβπ΄) β π₯) |
33 | 32 | ex 414 |
. . . . 5
β’ (π΄ β βͺ (π
1 β On) β ((π₯ β On β§ βπ¦ β π΄ (rankβπ¦) β π₯) β (rankβπ΄) β π₯)) |
34 | 33 | alrimiv 1931 |
. . . 4
β’ (π΄ β βͺ (π
1 β On) β βπ₯((π₯ β On β§ βπ¦ β π΄ (rankβπ¦) β π₯) β (rankβπ΄) β π₯)) |
35 | | ssintab 4930 |
. . . 4
β’
((rankβπ΄)
β β© {π₯ β£ (π₯ β On β§ βπ¦ β π΄ (rankβπ¦) β π₯)} β βπ₯((π₯ β On β§ βπ¦ β π΄ (rankβπ¦) β π₯) β (rankβπ΄) β π₯)) |
36 | 34, 35 | sylibr 233 |
. . 3
β’ (π΄ β βͺ (π
1 β On) β
(rankβπ΄) β
β© {π₯ β£ (π₯ β On β§ βπ¦ β π΄ (rankβπ¦) β π₯)}) |
37 | | df-rab 3407 |
. . . 4
β’ {π₯ β On β£ βπ¦ β π΄ (rankβπ¦) β π₯} = {π₯ β£ (π₯ β On β§ βπ¦ β π΄ (rankβπ¦) β π₯)} |
38 | 37 | inteqi 4915 |
. . 3
β’ β© {π₯
β On β£ βπ¦
β π΄ (rankβπ¦) β π₯} = β© {π₯ β£ (π₯ β On β§ βπ¦ β π΄ (rankβπ¦) β π₯)} |
39 | 36, 38 | sseqtrrdi 3999 |
. 2
β’ (π΄ β βͺ (π
1 β On) β
(rankβπ΄) β
β© {π₯ β On β£ βπ¦ β π΄ (rankβπ¦) β π₯}) |
40 | | rankelb 9768 |
. . . 4
β’ (π΄ β βͺ (π
1 β On) β (π¦ β π΄ β (rankβπ¦) β (rankβπ΄))) |
41 | 40 | ralrimiv 3139 |
. . 3
β’ (π΄ β βͺ (π
1 β On) β βπ¦ β π΄ (rankβπ¦) β (rankβπ΄)) |
42 | | eleq2 2823 |
. . . . 5
β’ (π₯ = (rankβπ΄) β ((rankβπ¦) β π₯ β (rankβπ¦) β (rankβπ΄))) |
43 | 42 | ralbidv 3171 |
. . . 4
β’ (π₯ = (rankβπ΄) β (βπ¦ β π΄ (rankβπ¦) β π₯ β βπ¦ β π΄ (rankβπ¦) β (rankβπ΄))) |
44 | 43 | onintss 6372 |
. . 3
β’
((rankβπ΄)
β On β (βπ¦
β π΄ (rankβπ¦) β (rankβπ΄) β β© {π₯
β On β£ βπ¦
β π΄ (rankβπ¦) β π₯} β (rankβπ΄))) |
45 | 1, 41, 44 | mpsyl 68 |
. 2
β’ (π΄ β βͺ (π
1 β On) β β© {π₯
β On β£ βπ¦
β π΄ (rankβπ¦) β π₯} β (rankβπ΄)) |
46 | 39, 45 | eqssd 3965 |
1
β’ (π΄ β βͺ (π
1 β On) β
(rankβπ΄) = β© {π₯
β On β£ βπ¦
β π΄ (rankβπ¦) β π₯}) |