Step | Hyp | Ref
| Expression |
1 | | r1funlim 9709 |
. . . . 5
β’ (Fun
π
1 β§ Lim dom π
1) |
2 | 1 | simpri 487 |
. . . 4
β’ Lim dom
π
1 |
3 | | limord 6382 |
. . . 4
β’ (Lim dom
π
1 β Ord dom π
1) |
4 | 2, 3 | ax-mp 5 |
. . 3
β’ Ord dom
π
1 |
5 | | ordelon 6346 |
. . 3
β’ ((Ord dom
π
1 β§ π΄ β dom π
1) β
π΄ β
On) |
6 | 4, 5 | mpan 689 |
. 2
β’ (π΄ β dom
π
1 β π΄ β On) |
7 | | eleq1 2826 |
. . . 4
β’ (π₯ = π¦ β (π₯ β dom π
1 β
π¦ β dom
π
1)) |
8 | | eleq1 2826 |
. . . . 5
β’ (π₯ = π¦ β (π₯ β βͺ
(π
1 β On) β π¦ β βͺ
(π
1 β On))) |
9 | | fveq2 6847 |
. . . . . 6
β’ (π₯ = π¦ β (rankβπ₯) = (rankβπ¦)) |
10 | | id 22 |
. . . . . 6
β’ (π₯ = π¦ β π₯ = π¦) |
11 | 9, 10 | eqeq12d 2753 |
. . . . 5
β’ (π₯ = π¦ β ((rankβπ₯) = π₯ β (rankβπ¦) = π¦)) |
12 | 8, 11 | anbi12d 632 |
. . . 4
β’ (π₯ = π¦ β ((π₯ β βͺ
(π
1 β On) β§ (rankβπ₯) = π₯) β (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦))) |
13 | 7, 12 | imbi12d 345 |
. . 3
β’ (π₯ = π¦ β ((π₯ β dom π
1 β
(π₯ β βͺ (π
1 β On) β§
(rankβπ₯) = π₯)) β (π¦ β dom π
1 β
(π¦ β βͺ (π
1 β On) β§
(rankβπ¦) = π¦)))) |
14 | | eleq1 2826 |
. . . 4
β’ (π₯ = π΄ β (π₯ β dom π
1 β
π΄ β dom
π
1)) |
15 | | eleq1 2826 |
. . . . 5
β’ (π₯ = π΄ β (π₯ β βͺ
(π
1 β On) β π΄ β βͺ
(π
1 β On))) |
16 | | fveq2 6847 |
. . . . . 6
β’ (π₯ = π΄ β (rankβπ₯) = (rankβπ΄)) |
17 | | id 22 |
. . . . . 6
β’ (π₯ = π΄ β π₯ = π΄) |
18 | 16, 17 | eqeq12d 2753 |
. . . . 5
β’ (π₯ = π΄ β ((rankβπ₯) = π₯ β (rankβπ΄) = π΄)) |
19 | 15, 18 | anbi12d 632 |
. . . 4
β’ (π₯ = π΄ β ((π₯ β βͺ
(π
1 β On) β§ (rankβπ₯) = π₯) β (π΄ β βͺ
(π
1 β On) β§ (rankβπ΄) = π΄))) |
20 | 14, 19 | imbi12d 345 |
. . 3
β’ (π₯ = π΄ β ((π₯ β dom π
1 β
(π₯ β βͺ (π
1 β On) β§
(rankβπ₯) = π₯)) β (π΄ β dom π
1 β
(π΄ β βͺ (π
1 β On) β§
(rankβπ΄) = π΄)))) |
21 | | ordtr1 6365 |
. . . . . . . . . 10
β’ (Ord dom
π
1 β ((π¦ β π₯ β§ π₯ β dom π
1) β
π¦ β dom
π
1)) |
22 | 4, 21 | ax-mp 5 |
. . . . . . . . 9
β’ ((π¦ β π₯ β§ π₯ β dom π
1) β
π¦ β dom
π
1) |
23 | 22 | ancoms 460 |
. . . . . . . 8
β’ ((π₯ β dom
π
1 β§ π¦ β π₯) β π¦ β dom
π
1) |
24 | | pm5.5 362 |
. . . . . . . 8
β’ (π¦ β dom
π
1 β ((π¦ β dom π
1 β
(π¦ β βͺ (π
1 β On) β§
(rankβπ¦) = π¦)) β (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦))) |
25 | 23, 24 | syl 17 |
. . . . . . 7
β’ ((π₯ β dom
π
1 β§ π¦ β π₯) β ((π¦ β dom π
1 β
(π¦ β βͺ (π
1 β On) β§
(rankβπ¦) = π¦)) β (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦))) |
26 | 25 | ralbidva 3173 |
. . . . . 6
β’ (π₯ β dom
π
1 β (βπ¦ β π₯ (π¦ β dom π
1 β
(π¦ β βͺ (π
1 β On) β§
(rankβπ¦) = π¦)) β βπ¦ β π₯ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦))) |
27 | | simplr 768 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ β dom
π
1 β§ π¦ β π₯) β§ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦)) β π¦ β π₯) |
28 | | ordelon 6346 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((Ord dom
π
1 β§ π₯ β dom π
1) β
π₯ β
On) |
29 | 4, 28 | mpan 689 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ β dom
π
1 β π₯ β On) |
30 | 29 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π₯ β dom
π
1 β§ π¦ β π₯) β§ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦)) β π₯ β On) |
31 | | eloni 6332 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β On β Ord π₯) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π₯ β dom
π
1 β§ π¦ β π₯) β§ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦)) β Ord π₯) |
33 | | ordelsuc 7760 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π¦ β π₯ β§ Ord π₯) β (π¦ β π₯ β suc π¦ β π₯)) |
34 | 27, 32, 33 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ β dom
π
1 β§ π¦ β π₯) β§ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦)) β (π¦ β π₯ β suc π¦ β π₯)) |
35 | 27, 34 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β dom
π
1 β§ π¦ β π₯) β§ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦)) β suc π¦ β π₯) |
36 | 23 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π₯ β dom
π
1 β§ π¦ β π₯) β§ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦)) β π¦ β dom
π
1) |
37 | | limsuc 7790 |
. . . . . . . . . . . . . . . . . . . 20
β’ (Lim dom
π
1 β (π¦ β dom π
1 β suc
π¦ β dom
π
1)) |
38 | 2, 37 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ β dom
π
1 β suc π¦ β dom
π
1) |
39 | 36, 38 | sylib 217 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ β dom
π
1 β§ π¦ β π₯) β§ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦)) β suc π¦ β dom
π
1) |
40 | | simpll 766 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ β dom
π
1 β§ π¦ β π₯) β§ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦)) β π₯ β dom
π
1) |
41 | | r1ord3g 9722 |
. . . . . . . . . . . . . . . . . 18
β’ ((suc
π¦ β dom
π
1 β§ π₯ β dom π
1) β
(suc π¦ β π₯ β
(π
1βsuc π¦) β (π
1βπ₯))) |
42 | 39, 40, 41 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β dom
π
1 β§ π¦ β π₯) β§ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦)) β (suc π¦ β π₯ β (π
1βsuc
π¦) β
(π
1βπ₯))) |
43 | 35, 42 | mpd 15 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β dom
π
1 β§ π¦ β π₯) β§ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦)) β (π
1βsuc
π¦) β
(π
1βπ₯)) |
44 | | rankidb 9743 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β βͺ (π
1 β On) β π¦ β
(π
1βsuc (rankβπ¦))) |
45 | 44 | ad2antrl 727 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β dom
π
1 β§ π¦ β π₯) β§ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦)) β π¦ β (π
1βsuc
(rankβπ¦))) |
46 | | suceq 6388 |
. . . . . . . . . . . . . . . . . . 19
β’
((rankβπ¦) =
π¦ β suc
(rankβπ¦) = suc π¦) |
47 | 46 | ad2antll 728 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ β dom
π
1 β§ π¦ β π₯) β§ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦)) β suc (rankβπ¦) = suc π¦) |
48 | 47 | fveq2d 6851 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β dom
π
1 β§ π¦ β π₯) β§ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦)) β (π
1βsuc
(rankβπ¦)) =
(π
1βsuc π¦)) |
49 | 45, 48 | eleqtrd 2840 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β dom
π
1 β§ π¦ β π₯) β§ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦)) β π¦ β (π
1βsuc
π¦)) |
50 | 43, 49 | sseldd 3950 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β dom
π
1 β§ π¦ β π₯) β§ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦)) β π¦ β (π
1βπ₯)) |
51 | 50 | ex 414 |
. . . . . . . . . . . . . 14
β’ ((π₯ β dom
π
1 β§ π¦ β π₯) β ((π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦) β π¦ β (π
1βπ₯))) |
52 | 51 | ralimdva 3165 |
. . . . . . . . . . . . 13
β’ (π₯ β dom
π
1 β (βπ¦ β π₯ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦) β βπ¦ β π₯ π¦ β (π
1βπ₯))) |
53 | 52 | imp 408 |
. . . . . . . . . . . 12
β’ ((π₯ β dom
π
1 β§ βπ¦ β π₯ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦)) β βπ¦ β π₯ π¦ β (π
1βπ₯)) |
54 | | dfss3 3937 |
. . . . . . . . . . . 12
β’ (π₯ β
(π
1βπ₯) β βπ¦ β π₯ π¦ β (π
1βπ₯)) |
55 | 53, 54 | sylibr 233 |
. . . . . . . . . . 11
β’ ((π₯ β dom
π
1 β§ βπ¦ β π₯ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦)) β π₯ β (π
1βπ₯)) |
56 | | vex 3452 |
. . . . . . . . . . . 12
β’ π₯ β V |
57 | 56 | elpw 4569 |
. . . . . . . . . . 11
β’ (π₯ β π«
(π
1βπ₯) β π₯ β (π
1βπ₯)) |
58 | 55, 57 | sylibr 233 |
. . . . . . . . . 10
β’ ((π₯ β dom
π
1 β§ βπ¦ β π₯ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦)) β π₯ β π«
(π
1βπ₯)) |
59 | | r1sucg 9712 |
. . . . . . . . . . 11
β’ (π₯ β dom
π
1 β (π
1βsuc π₯) = π«
(π
1βπ₯)) |
60 | 59 | adantr 482 |
. . . . . . . . . 10
β’ ((π₯ β dom
π
1 β§ βπ¦ β π₯ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦)) β (π
1βsuc
π₯) = π«
(π
1βπ₯)) |
61 | 58, 60 | eleqtrrd 2841 |
. . . . . . . . 9
β’ ((π₯ β dom
π
1 β§ βπ¦ β π₯ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦)) β π₯ β (π
1βsuc
π₯)) |
62 | | r1elwf 9739 |
. . . . . . . . 9
β’ (π₯ β
(π
1βsuc π₯) β π₯ β βͺ
(π
1 β On)) |
63 | 61, 62 | syl 17 |
. . . . . . . 8
β’ ((π₯ β dom
π
1 β§ βπ¦ β π₯ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦)) β π₯ β βͺ
(π
1 β On)) |
64 | | rankval3b 9769 |
. . . . . . . . . 10
β’ (π₯ β βͺ (π
1 β On) β
(rankβπ₯) = β© {π§
β On β£ βπ¦
β π₯ (rankβπ¦) β π§}) |
65 | 63, 64 | syl 17 |
. . . . . . . . 9
β’ ((π₯ β dom
π
1 β§ βπ¦ β π₯ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦)) β (rankβπ₯) = β© {π§ β On β£ βπ¦ β π₯ (rankβπ¦) β π§}) |
66 | | eleq1 2826 |
. . . . . . . . . . . . . . . 16
β’
((rankβπ¦) =
π¦ β ((rankβπ¦) β π§ β π¦ β π§)) |
67 | 66 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π¦ β βͺ (π
1 β On) β§
(rankβπ¦) = π¦) β ((rankβπ¦) β π§ β π¦ β π§)) |
68 | 67 | ralimi 3087 |
. . . . . . . . . . . . . 14
β’
(βπ¦ β
π₯ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦) β βπ¦ β π₯ ((rankβπ¦) β π§ β π¦ β π§)) |
69 | | ralbi 3107 |
. . . . . . . . . . . . . 14
β’
(βπ¦ β
π₯ ((rankβπ¦) β π§ β π¦ β π§) β (βπ¦ β π₯ (rankβπ¦) β π§ β βπ¦ β π₯ π¦ β π§)) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . 13
β’
(βπ¦ β
π₯ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦) β (βπ¦ β π₯ (rankβπ¦) β π§ β βπ¦ β π₯ π¦ β π§)) |
71 | | dfss3 3937 |
. . . . . . . . . . . . 13
β’ (π₯ β π§ β βπ¦ β π₯ π¦ β π§) |
72 | 70, 71 | bitr4di 289 |
. . . . . . . . . . . 12
β’
(βπ¦ β
π₯ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦) β (βπ¦ β π₯ (rankβπ¦) β π§ β π₯ β π§)) |
73 | 72 | rabbidv 3418 |
. . . . . . . . . . 11
β’
(βπ¦ β
π₯ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦) β {π§ β On β£ βπ¦ β π₯ (rankβπ¦) β π§} = {π§ β On β£ π₯ β π§}) |
74 | 73 | inteqd 4917 |
. . . . . . . . . 10
β’
(βπ¦ β
π₯ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦) β β© {π§ β On β£ βπ¦ β π₯ (rankβπ¦) β π§} = β© {π§ β On β£ π₯ β π§}) |
75 | 74 | adantl 483 |
. . . . . . . . 9
β’ ((π₯ β dom
π
1 β§ βπ¦ β π₯ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦)) β β© {π§ β On β£ βπ¦ β π₯ (rankβπ¦) β π§} = β© {π§ β On β£ π₯ β π§}) |
76 | 29 | adantr 482 |
. . . . . . . . . 10
β’ ((π₯ β dom
π
1 β§ βπ¦ β π₯ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦)) β π₯ β On) |
77 | | intmin 4934 |
. . . . . . . . . 10
β’ (π₯ β On β β© {π§
β On β£ π₯ β
π§} = π₯) |
78 | 76, 77 | syl 17 |
. . . . . . . . 9
β’ ((π₯ β dom
π
1 β§ βπ¦ β π₯ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦)) β β© {π§ β On β£ π₯ β π§} = π₯) |
79 | 65, 75, 78 | 3eqtrd 2781 |
. . . . . . . 8
β’ ((π₯ β dom
π
1 β§ βπ¦ β π₯ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦)) β (rankβπ₯) = π₯) |
80 | 63, 79 | jca 513 |
. . . . . . 7
β’ ((π₯ β dom
π
1 β§ βπ¦ β π₯ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦)) β (π₯ β βͺ
(π
1 β On) β§ (rankβπ₯) = π₯)) |
81 | 80 | ex 414 |
. . . . . 6
β’ (π₯ β dom
π
1 β (βπ¦ β π₯ (π¦ β βͺ
(π
1 β On) β§ (rankβπ¦) = π¦) β (π₯ β βͺ
(π
1 β On) β§ (rankβπ₯) = π₯))) |
82 | 26, 81 | sylbid 239 |
. . . . 5
β’ (π₯ β dom
π
1 β (βπ¦ β π₯ (π¦ β dom π
1 β
(π¦ β βͺ (π
1 β On) β§
(rankβπ¦) = π¦)) β (π₯ β βͺ
(π
1 β On) β§ (rankβπ₯) = π₯))) |
83 | 82 | com12 32 |
. . . 4
β’
(βπ¦ β
π₯ (π¦ β dom π
1 β
(π¦ β βͺ (π
1 β On) β§
(rankβπ¦) = π¦)) β (π₯ β dom π
1 β
(π₯ β βͺ (π
1 β On) β§
(rankβπ₯) = π₯))) |
84 | 83 | a1i 11 |
. . 3
β’ (π₯ β On β (βπ¦ β π₯ (π¦ β dom π
1 β
(π¦ β βͺ (π
1 β On) β§
(rankβπ¦) = π¦)) β (π₯ β dom π
1 β
(π₯ β βͺ (π
1 β On) β§
(rankβπ₯) = π₯)))) |
85 | 13, 20, 84 | tfis3 7799 |
. 2
β’ (π΄ β On β (π΄ β dom
π
1 β (π΄ β βͺ
(π
1 β On) β§ (rankβπ΄) = π΄))) |
86 | 6, 85 | mpcom 38 |
1
β’ (π΄ β dom
π
1 β (π΄ β βͺ
(π
1 β On) β§ (rankβπ΄) = π΄)) |