Step | Hyp | Ref
| Expression |
1 | | hsmexlem4.s |
. . . . . . . 8
β’ π = {π β βͺ
(π
1 β On) β£ βπ β (TCβ{π})π βΌ π} |
2 | 1 | ssrab3 4080 |
. . . . . . 7
β’ π β βͺ (π
1 β On) |
3 | 2 | sseli 3978 |
. . . . . 6
β’ (π β π β π β βͺ
(π
1 β On)) |
4 | | tcrank 9878 |
. . . . . 6
β’ (π β βͺ (π
1 β On) β
(rankβπ) = (rank
β (TCβπ))) |
5 | 3, 4 | syl 17 |
. . . . 5
β’ (π β π β (rankβπ) = (rank β (TCβπ))) |
6 | | hsmexlem4.u |
. . . . . . . 8
β’ π = (π₯ β V β¦ (rec((π¦ β V β¦ βͺ π¦),
π₯) βΎ
Ο)) |
7 | 6 | itunitc 10415 |
. . . . . . 7
β’
(TCβπ) = βͺ ran (πβπ) |
8 | 6 | itunifn 10411 |
. . . . . . . 8
β’ (π β π β (πβπ) Fn Ο) |
9 | | fniunfv 7245 |
. . . . . . . 8
β’ ((πβπ) Fn Ο β βͺ π β Ο ((πβπ)βπ) = βͺ ran (πβπ)) |
10 | 8, 9 | syl 17 |
. . . . . . 7
β’ (π β π β βͺ
π β Ο ((πβπ)βπ) = βͺ ran (πβπ)) |
11 | 7, 10 | eqtr4id 2791 |
. . . . . 6
β’ (π β π β (TCβπ) = βͺ π β Ο ((πβπ)βπ)) |
12 | 11 | imaeq2d 6059 |
. . . . 5
β’ (π β π β (rank β (TCβπ)) = (rank β βͺ π β Ο ((πβπ)βπ))) |
13 | | imaiun 7243 |
. . . . . 6
β’ (rank
β βͺ π β Ο ((πβπ)βπ)) = βͺ
π β Ο (rank
β ((πβπ)βπ)) |
14 | 13 | a1i 11 |
. . . . 5
β’ (π β π β (rank β βͺ π β Ο ((πβπ)βπ)) = βͺ
π β Ο (rank
β ((πβπ)βπ))) |
15 | 5, 12, 14 | 3eqtrd 2776 |
. . . 4
β’ (π β π β (rankβπ) = βͺ π β Ο (rank β
((πβπ)βπ))) |
16 | | dmresi 6051 |
. . . 4
β’ dom ( I
βΎ βͺ π β Ο (rank β ((πβπ)βπ))) = βͺ
π β Ο (rank
β ((πβπ)βπ)) |
17 | 15, 16 | eqtr4di 2790 |
. . 3
β’ (π β π β (rankβπ) = dom ( I βΎ βͺ π β Ο (rank β ((πβπ)βπ)))) |
18 | | rankon 9789 |
. . . . . 6
β’
(rankβπ)
β On |
19 | 15, 18 | eqeltrrdi 2842 |
. . . . 5
β’ (π β π β βͺ
π β Ο (rank
β ((πβπ)βπ)) β On) |
20 | | eloni 6374 |
. . . . 5
β’ (βͺ π β Ο (rank β ((πβπ)βπ)) β On β Ord βͺ π β Ο (rank β ((πβπ)βπ))) |
21 | | oiid 9535 |
. . . . 5
β’ (Ord
βͺ π β Ο (rank β ((πβπ)βπ)) β OrdIso( E , βͺ π β Ο (rank β ((πβπ)βπ))) = ( I βΎ βͺ π β Ο (rank β ((πβπ)βπ)))) |
22 | 19, 20, 21 | 3syl 18 |
. . . 4
β’ (π β π β OrdIso( E , βͺ π β Ο (rank β ((πβπ)βπ))) = ( I βΎ βͺ π β Ο (rank β ((πβπ)βπ)))) |
23 | 22 | dmeqd 5905 |
. . 3
β’ (π β π β dom OrdIso( E , βͺ π β Ο (rank β ((πβπ)βπ))) = dom ( I βΎ βͺ π β Ο (rank β ((πβπ)βπ)))) |
24 | 17, 23 | eqtr4d 2775 |
. 2
β’ (π β π β (rankβπ) = dom OrdIso( E , βͺ π β Ο (rank β ((πβπ)βπ)))) |
25 | | omex 9637 |
. . . 4
β’ Ο
β V |
26 | | wdomref 9566 |
. . . 4
β’ (Ο
β V β Ο βΌ* Ο) |
27 | 25, 26 | mp1i 13 |
. . 3
β’ (π β π β Ο βΌ*
Ο) |
28 | | frfnom 8434 |
. . . . . . 7
β’
(rec((π§ β V
β¦ (harβπ« (π Γ π§))), (harβπ« π)) βΎ Ο) Fn
Ο |
29 | | hsmexlem4.h |
. . . . . . . 8
β’ π» = (rec((π§ β V β¦ (harβπ« (π Γ π§))), (harβπ« π)) βΎ Ο) |
30 | 29 | fneq1i 6646 |
. . . . . . 7
β’ (π» Fn Ο β (rec((π§ β V β¦
(harβπ« (π
Γ π§))),
(harβπ« π))
βΎ Ο) Fn Ο) |
31 | 28, 30 | mpbir 230 |
. . . . . 6
β’ π» Fn Ο |
32 | | fniunfv 7245 |
. . . . . 6
β’ (π» Fn Ο β βͺ π β Ο (π»βπ) = βͺ ran π») |
33 | 31, 32 | ax-mp 5 |
. . . . 5
β’ βͺ π β Ο (π»βπ) = βͺ ran π» |
34 | | iunon 8338 |
. . . . . . 7
β’ ((Ο
β V β§ βπ
β Ο (π»βπ) β On) β βͺ π β Ο (π»βπ) β On) |
35 | 25, 34 | mpan 688 |
. . . . . 6
β’
(βπ β
Ο (π»βπ) β On β βͺ π β Ο (π»βπ) β On) |
36 | 29 | hsmexlem9 10419 |
. . . . . 6
β’ (π β Ο β (π»βπ) β On) |
37 | 35, 36 | mprg 3067 |
. . . . 5
β’ βͺ π β Ο (π»βπ) β On |
38 | 33, 37 | eqeltrri 2830 |
. . . 4
β’ βͺ ran π» β On |
39 | 38 | a1i 11 |
. . 3
β’ (π β π β βͺ ran
π» β
On) |
40 | | fvssunirn 6924 |
. . . . . 6
β’ (π»βπ) β βͺ ran
π» |
41 | | hsmexlem4.x |
. . . . . . . 8
β’ π β V |
42 | | eqid 2732 |
. . . . . . . 8
β’ OrdIso( E
, (rank β ((πβπ)βπ))) = OrdIso( E , (rank β ((πβπ)βπ))) |
43 | 41, 29, 6, 1, 42 | hsmexlem4 10423 |
. . . . . . 7
β’ ((π β Ο β§ π β π) β dom OrdIso( E , (rank β
((πβπ)βπ))) β (π»βπ)) |
44 | 43 | ancoms 459 |
. . . . . 6
β’ ((π β π β§ π β Ο) β dom OrdIso( E , (rank
β ((πβπ)βπ))) β (π»βπ)) |
45 | 40, 44 | sselid 3980 |
. . . . 5
β’ ((π β π β§ π β Ο) β dom OrdIso( E , (rank
β ((πβπ)βπ))) β βͺ ran
π») |
46 | | imassrn 6070 |
. . . . . . 7
β’ (rank
β ((πβπ)βπ)) β ran rank |
47 | | rankf 9788 |
. . . . . . . 8
β’
rank:βͺ (π
1 β
On)βΆOn |
48 | | frn 6724 |
. . . . . . . 8
β’
(rank:βͺ (π
1 β
On)βΆOn β ran rank β On) |
49 | 47, 48 | ax-mp 5 |
. . . . . . 7
β’ ran rank
β On |
50 | 46, 49 | sstri 3991 |
. . . . . 6
β’ (rank
β ((πβπ)βπ)) β On |
51 | | ffun 6720 |
. . . . . . . 8
β’
(rank:βͺ (π
1 β
On)βΆOn β Fun rank) |
52 | | fvex 6904 |
. . . . . . . . 9
β’ ((πβπ)βπ) β V |
53 | 52 | funimaex 6636 |
. . . . . . . 8
β’ (Fun rank
β (rank β ((πβπ)βπ)) β V) |
54 | 47, 51, 53 | mp2b 10 |
. . . . . . 7
β’ (rank
β ((πβπ)βπ)) β V |
55 | 54 | elpw 4606 |
. . . . . 6
β’ ((rank
β ((πβπ)βπ)) β π« On β (rank β
((πβπ)βπ)) β On) |
56 | 50, 55 | mpbir 230 |
. . . . 5
β’ (rank
β ((πβπ)βπ)) β π« On |
57 | 45, 56 | jctil 520 |
. . . 4
β’ ((π β π β§ π β Ο) β ((rank β
((πβπ)βπ)) β π« On β§ dom OrdIso( E ,
(rank β ((πβπ)βπ))) β βͺ ran
π»)) |
58 | 57 | ralrimiva 3146 |
. . 3
β’ (π β π β βπ β Ο ((rank β ((πβπ)βπ)) β π« On β§ dom OrdIso( E ,
(rank β ((πβπ)βπ))) β βͺ ran
π»)) |
59 | | eqid 2732 |
. . . 4
β’ OrdIso( E
, βͺ π β Ο (rank β ((πβπ)βπ))) = OrdIso( E , βͺ π β Ο (rank β ((πβπ)βπ))) |
60 | 42, 59 | hsmexlem3 10422 |
. . 3
β’
(((Ο βΌ* Ο β§ βͺ ran π» β On) β§ βπ β Ο ((rank β ((πβπ)βπ)) β π« On β§ dom OrdIso( E ,
(rank β ((πβπ)βπ))) β βͺ ran
π»)) β dom OrdIso( E ,
βͺ π β Ο (rank β ((πβπ)βπ))) β (harβπ« (Ο
Γ βͺ ran π»))) |
61 | 27, 39, 58, 60 | syl21anc 836 |
. 2
β’ (π β π β dom OrdIso( E , βͺ π β Ο (rank β ((πβπ)βπ))) β (harβπ« (Ο
Γ βͺ ran π»))) |
62 | 24, 61 | eqeltrd 2833 |
1
β’ (π β π β (rankβπ) β (harβπ« (Ο
Γ βͺ ran π»))) |