Step | Hyp | Ref
| Expression |
1 | | suceq 6384 |
. . 3
β’ (π = (rankβπ) β suc π = suc (rankβπ)) |
2 | 1 | fveq2d 6847 |
. 2
β’ (π = (rankβπ) β (π§βsuc π) = (π§βsuc (rankβπ))) |
3 | | aomclem4.f |
. 2
β’ πΉ = {β¨π, πβ© β£ ((rankβπ) E (rankβπ) β¨ ((rankβπ) = (rankβπ) β§ π(π§βsuc (rankβπ))π))} |
4 | | r1fnon 9704 |
. . . . . . . . . . . . . 14
β’
π
1 Fn On |
5 | | fnfun 6603 |
. . . . . . . . . . . . . 14
β’
(π
1 Fn On β Fun
π
1) |
6 | 4, 5 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ Fun
π
1 |
7 | 4 | fndmi 6607 |
. . . . . . . . . . . . . 14
β’ dom
π
1 = On |
8 | 7 | eqimss2i 4004 |
. . . . . . . . . . . . 13
β’ On
β dom π
1 |
9 | 6, 8 | pm3.2i 472 |
. . . . . . . . . . . 12
β’ (Fun
π
1 β§ On β dom
π
1) |
10 | | aomclem4.on |
. . . . . . . . . . . 12
β’ (π β dom π§ β On) |
11 | | funfvima2 7182 |
. . . . . . . . . . . 12
β’ ((Fun
π
1 β§ On β dom π
1) β (dom
π§ β On β
(π
1βdom π§) β (π
1 β
On))) |
12 | 9, 10, 11 | mpsyl 68 |
. . . . . . . . . . 11
β’ (π β
(π
1βdom π§) β (π
1 β
On)) |
13 | | elssuni 4899 |
. . . . . . . . . . 11
β’
((π
1βdom π§) β (π
1 β On)
β (π
1βdom π§) β βͺ
(π
1 β On)) |
14 | 12, 13 | syl 17 |
. . . . . . . . . 10
β’ (π β
(π
1βdom π§) β βͺ
(π
1 β On)) |
15 | 14 | sselda 3945 |
. . . . . . . . 9
β’ ((π β§ π β (π
1βdom
π§)) β π β βͺ (π
1 β On)) |
16 | | rankidb 9737 |
. . . . . . . . 9
β’ (π β βͺ (π
1 β On) β π β
(π
1βsuc (rankβπ))) |
17 | 15, 16 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β (π
1βdom
π§)) β π β
(π
1βsuc (rankβπ))) |
18 | | suceq 6384 |
. . . . . . . . . 10
β’
((rankβπ) =
(rankβπ) β suc
(rankβπ) = suc
(rankβπ)) |
19 | 18 | fveq2d 6847 |
. . . . . . . . 9
β’
((rankβπ) =
(rankβπ) β
(π
1βsuc (rankβπ)) = (π
1βsuc
(rankβπ))) |
20 | 19 | eleq2d 2824 |
. . . . . . . 8
β’
((rankβπ) =
(rankβπ) β
(π β
(π
1βsuc (rankβπ)) β π β (π
1βsuc
(rankβπ)))) |
21 | 17, 20 | syl5ibcom 244 |
. . . . . . 7
β’ ((π β§ π β (π
1βdom
π§)) β
((rankβπ) =
(rankβπ) β π β
(π
1βsuc (rankβπ)))) |
22 | 21 | expimpd 455 |
. . . . . 6
β’ (π β ((π β (π
1βdom
π§) β§ (rankβπ) = (rankβπ)) β π β (π
1βsuc
(rankβπ)))) |
23 | 22 | ss2abdv 4021 |
. . . . 5
β’ (π β {π β£ (π β (π
1βdom
π§) β§ (rankβπ) = (rankβπ))} β {π β£ π β (π
1βsuc
(rankβπ))}) |
24 | | df-rab 3409 |
. . . . 5
β’ {π β
(π
1βdom π§) β£ (rankβπ) = (rankβπ)} = {π β£ (π β (π
1βdom
π§) β§ (rankβπ) = (rankβπ))} |
25 | | abid1 2875 |
. . . . 5
β’
(π
1βsuc (rankβπ)) = {π β£ π β (π
1βsuc
(rankβπ))} |
26 | 23, 24, 25 | 3sstr4g 3990 |
. . . 4
β’ (π β {π β (π
1βdom
π§) β£
(rankβπ) =
(rankβπ)} β
(π
1βsuc (rankβπ))) |
27 | 26 | adantr 482 |
. . 3
β’ ((π β§ π β (π
1βdom
π§)) β {π β
(π
1βdom π§) β£ (rankβπ) = (rankβπ)} β (π
1βsuc
(rankβπ))) |
28 | | fveq2 6843 |
. . . . 5
β’ (π = suc (rankβπ) β (π§βπ) = (π§βsuc (rankβπ))) |
29 | | fveq2 6843 |
. . . . 5
β’ (π = suc (rankβπ) β
(π
1βπ) = (π
1βsuc
(rankβπ))) |
30 | 28, 29 | weeq12d 41370 |
. . . 4
β’ (π = suc (rankβπ) β ((π§βπ) We (π
1βπ) β (π§βsuc (rankβπ)) We (π
1βsuc
(rankβπ)))) |
31 | | aomclem4.we |
. . . . . 6
β’ (π β βπ β dom π§(π§βπ) We (π
1βπ)) |
32 | | fveq2 6843 |
. . . . . . . 8
β’ (π = π β (π§βπ) = (π§βπ)) |
33 | | fveq2 6843 |
. . . . . . . 8
β’ (π = π β (π
1βπ) =
(π
1βπ)) |
34 | 32, 33 | weeq12d 41370 |
. . . . . . 7
β’ (π = π β ((π§βπ) We (π
1βπ) β (π§βπ) We (π
1βπ))) |
35 | 34 | cbvralvw 3226 |
. . . . . 6
β’
(βπ β
dom π§(π§βπ) We (π
1βπ) β βπ β dom π§(π§βπ) We (π
1βπ)) |
36 | 31, 35 | sylib 217 |
. . . . 5
β’ (π β βπ β dom π§(π§βπ) We (π
1βπ)) |
37 | 36 | adantr 482 |
. . . 4
β’ ((π β§ π β (π
1βdom
π§)) β βπ β dom π§(π§βπ) We (π
1βπ)) |
38 | | rankr1ai 9735 |
. . . . . 6
β’ (π β
(π
1βdom π§) β (rankβπ) β dom π§) |
39 | 38 | adantl 483 |
. . . . 5
β’ ((π β§ π β (π
1βdom
π§)) β
(rankβπ) β dom
π§) |
40 | | eloni 6328 |
. . . . . . . 8
β’ (dom
π§ β On β Ord dom
π§) |
41 | 10, 40 | syl 17 |
. . . . . . 7
β’ (π β Ord dom π§) |
42 | | aomclem4.su |
. . . . . . 7
β’ (π β dom π§ = βͺ dom π§) |
43 | | limsuc2 41371 |
. . . . . . 7
β’ ((Ord dom
π§ β§ dom π§ = βͺ
dom π§) β
((rankβπ) β dom
π§ β suc
(rankβπ) β dom
π§)) |
44 | 41, 42, 43 | syl2anc 585 |
. . . . . 6
β’ (π β ((rankβπ) β dom π§ β suc (rankβπ) β dom π§)) |
45 | 44 | adantr 482 |
. . . . 5
β’ ((π β§ π β (π
1βdom
π§)) β
((rankβπ) β dom
π§ β suc
(rankβπ) β dom
π§)) |
46 | 39, 45 | mpbid 231 |
. . . 4
β’ ((π β§ π β (π
1βdom
π§)) β suc
(rankβπ) β dom
π§) |
47 | 30, 37, 46 | rspcdva 3583 |
. . 3
β’ ((π β§ π β (π
1βdom
π§)) β (π§βsuc (rankβπ)) We
(π
1βsuc (rankβπ))) |
48 | | wess 5621 |
. . 3
β’ ({π β
(π
1βdom π§) β£ (rankβπ) = (rankβπ)} β (π
1βsuc
(rankβπ)) β
((π§βsuc
(rankβπ)) We
(π
1βsuc (rankβπ)) β (π§βsuc (rankβπ)) We {π β (π
1βdom
π§) β£
(rankβπ) =
(rankβπ)})) |
49 | 27, 47, 48 | sylc 65 |
. 2
β’ ((π β§ π β (π
1βdom
π§)) β (π§βsuc (rankβπ)) We {π β (π
1βdom
π§) β£
(rankβπ) =
(rankβπ)}) |
50 | | rankf 9731 |
. . . 4
β’
rank:βͺ (π
1 β
On)βΆOn |
51 | 50 | a1i 11 |
. . 3
β’ (π β rank:βͺ (π
1 β
On)βΆOn) |
52 | 51, 14 | fssresd 6710 |
. 2
β’ (π β (rank βΎ
(π
1βdom π§)):(π
1βdom π§)βΆOn) |
53 | | epweon 7710 |
. . 3
β’ E We
On |
54 | 53 | a1i 11 |
. 2
β’ (π β E We On) |
55 | 2, 3, 49, 52, 54 | fnwe2 41383 |
1
β’ (π β πΉ We (π
1βdom π§)) |