Step | Hyp | Ref
| Expression |
1 | | hsmexlem4.s |
. . . . . . . 8
β’ π = {π β βͺ
(π
1 β On) β£ βπ β (TCβ{π})π βΌ π} |
2 | 1 | ssrab3 4044 |
. . . . . . 7
β’ π β βͺ (π
1 β On) |
3 | 2 | sseli 3944 |
. . . . . 6
β’ (π β π β π β βͺ
(π
1 β On)) |
4 | | tcrank 9828 |
. . . . . 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 10365 |
. . . . . . 7
β’
(TCβπ) = βͺ ran (πβπ) |
8 | 6 | itunifn 10361 |
. . . . . . . 8
β’ (π β π β (πβπ) Fn Ο) |
9 | | fniunfv 7198 |
. . . . . . . 8
β’ ((πβπ) Fn Ο β βͺ π β Ο ((πβπ)βπ) = βͺ ran (πβπ)) |
10 | 8, 9 | syl 17 |
. . . . . . 7
β’ (π β π β βͺ
π β Ο ((πβπ)βπ) = βͺ ran (πβπ)) |
11 | 7, 10 | eqtr4id 2792 |
. . . . . 6
β’ (π β π β (TCβπ) = βͺ π β Ο ((πβπ)βπ)) |
12 | 11 | imaeq2d 6017 |
. . . . 5
β’ (π β π β (rank β (TCβπ)) = (rank β βͺ π β Ο ((πβπ)βπ))) |
13 | | imaiun 7196 |
. . . . . 6
β’ (rank
β βͺ π β Ο ((πβπ)βπ)) = βͺ
π β Ο (rank
β ((πβπ)βπ)) |
14 | 13 | a1i 11 |
. . . . 5
β’ (π β π β (rank β βͺ π β Ο ((πβπ)βπ)) = βͺ
π β Ο (rank
β ((πβπ)βπ))) |
15 | 5, 12, 14 | 3eqtrd 2777 |
. . . 4
β’ (π β π β (rankβπ) = βͺ π β Ο (rank β
((πβπ)βπ))) |
16 | | dmresi 6009 |
. . . 4
β’ dom ( I
βΎ βͺ π β Ο (rank β ((πβπ)βπ))) = βͺ
π β Ο (rank
β ((πβπ)βπ)) |
17 | 15, 16 | eqtr4di 2791 |
. . 3
β’ (π β π β (rankβπ) = dom ( I βΎ βͺ π β Ο (rank β ((πβπ)βπ)))) |
18 | | rankon 9739 |
. . . . . 6
β’
(rankβπ)
β On |
19 | 15, 18 | eqeltrrdi 2843 |
. . . . 5
β’ (π β π β βͺ
π β Ο (rank
β ((πβπ)βπ)) β On) |
20 | | eloni 6331 |
. . . . 5
β’ (βͺ π β Ο (rank β ((πβπ)βπ)) β On β Ord βͺ π β Ο (rank β ((πβπ)βπ))) |
21 | | oiid 9485 |
. . . . 5
β’ (Ord
βͺ π β Ο (rank β ((πβπ)βπ)) β OrdIso( E , βͺ π β Ο (rank β ((πβπ)βπ))) = ( I βΎ βͺ π β Ο (rank β ((πβπ)βπ)))) |
22 | 19, 20, 21 | 3syl 18 |
. . . 4
β’ (π β π β OrdIso( E , βͺ π β Ο (rank β ((πβπ)βπ))) = ( I βΎ βͺ π β Ο (rank β ((πβπ)βπ)))) |
23 | 22 | dmeqd 5865 |
. . 3
β’ (π β π β dom OrdIso( E , βͺ π β Ο (rank β ((πβπ)βπ))) = dom ( I βΎ βͺ π β Ο (rank β ((πβπ)βπ)))) |
24 | 17, 23 | eqtr4d 2776 |
. 2
β’ (π β π β (rankβπ) = dom OrdIso( E , βͺ π β Ο (rank β ((πβπ)βπ)))) |
25 | | omex 9587 |
. . . 4
β’ Ο
β V |
26 | | wdomref 9516 |
. . . 4
β’ (Ο
β V β Ο βΌ* Ο) |
27 | 25, 26 | mp1i 13 |
. . 3
β’ (π β π β Ο βΌ*
Ο) |
28 | | frfnom 8385 |
. . . . . . 7
β’
(rec((π§ β V
β¦ (harβπ« (π Γ π§))), (harβπ« π)) βΎ Ο) Fn
Ο |
29 | | hsmexlem4.h |
. . . . . . . 8
β’ π» = (rec((π§ β V β¦ (harβπ« (π Γ π§))), (harβπ« π)) βΎ Ο) |
30 | 29 | fneq1i 6603 |
. . . . . . 7
β’ (π» Fn Ο β (rec((π§ β V β¦
(harβπ« (π
Γ π§))),
(harβπ« π))
βΎ Ο) Fn Ο) |
31 | 28, 30 | mpbir 230 |
. . . . . 6
β’ π» Fn Ο |
32 | | fniunfv 7198 |
. . . . . 6
β’ (π» Fn Ο β βͺ π β Ο (π»βπ) = βͺ ran π») |
33 | 31, 32 | ax-mp 5 |
. . . . 5
β’ βͺ π β Ο (π»βπ) = βͺ ran π» |
34 | | iunon 8289 |
. . . . . . 7
β’ ((Ο
β V β§ βπ
β Ο (π»βπ) β On) β βͺ π β Ο (π»βπ) β On) |
35 | 25, 34 | mpan 689 |
. . . . . 6
β’
(βπ β
Ο (π»βπ) β On β βͺ π β Ο (π»βπ) β On) |
36 | 29 | hsmexlem9 10369 |
. . . . . 6
β’ (π β Ο β (π»βπ) β On) |
37 | 35, 36 | mprg 3067 |
. . . . 5
β’ βͺ π β Ο (π»βπ) β On |
38 | 33, 37 | eqeltrri 2831 |
. . . 4
β’ βͺ ran π» β On |
39 | 38 | a1i 11 |
. . 3
β’ (π β π β βͺ ran
π» β
On) |
40 | | fvssunirn 6879 |
. . . . . 6
β’ (π»βπ) β βͺ ran
π» |
41 | | hsmexlem4.x |
. . . . . . . 8
β’ π β V |
42 | | eqid 2733 |
. . . . . . . 8
β’ OrdIso( E
, (rank β ((πβπ)βπ))) = OrdIso( E , (rank β ((πβπ)βπ))) |
43 | 41, 29, 6, 1, 42 | hsmexlem4 10373 |
. . . . . . 7
β’ ((π β Ο β§ π β π) β dom OrdIso( E , (rank β
((πβπ)βπ))) β (π»βπ)) |
44 | 43 | ancoms 460 |
. . . . . 6
β’ ((π β π β§ π β Ο) β dom OrdIso( E , (rank
β ((πβπ)βπ))) β (π»βπ)) |
45 | 40, 44 | sselid 3946 |
. . . . 5
β’ ((π β π β§ π β Ο) β dom OrdIso( E , (rank
β ((πβπ)βπ))) β βͺ ran
π») |
46 | | imassrn 6028 |
. . . . . . 7
β’ (rank
β ((πβπ)βπ)) β ran rank |
47 | | rankf 9738 |
. . . . . . . 8
β’
rank:βͺ (π
1 β
On)βΆOn |
48 | | frn 6679 |
. . . . . . . 8
β’
(rank:βͺ (π
1 β
On)βΆOn β ran rank β On) |
49 | 47, 48 | ax-mp 5 |
. . . . . . 7
β’ ran rank
β On |
50 | 46, 49 | sstri 3957 |
. . . . . 6
β’ (rank
β ((πβπ)βπ)) β On |
51 | | ffun 6675 |
. . . . . . . 8
β’
(rank:βͺ (π
1 β
On)βΆOn β Fun rank) |
52 | | fvex 6859 |
. . . . . . . . 9
β’ ((πβπ)βπ) β V |
53 | 52 | funimaex 6593 |
. . . . . . . 8
β’ (Fun rank
β (rank β ((πβπ)βπ)) β V) |
54 | 47, 51, 53 | mp2b 10 |
. . . . . . 7
β’ (rank
β ((πβπ)βπ)) β V |
55 | 54 | elpw 4568 |
. . . . . 6
β’ ((rank
β ((πβπ)βπ)) β π« On β (rank β
((πβπ)βπ)) β On) |
56 | 50, 55 | mpbir 230 |
. . . . 5
β’ (rank
β ((πβπ)βπ)) β π« On |
57 | 45, 56 | jctil 521 |
. . . 4
β’ ((π β π β§ π β Ο) β ((rank β
((πβπ)βπ)) β π« On β§ dom OrdIso( E ,
(rank β ((πβπ)βπ))) β βͺ ran
π»)) |
58 | 57 | ralrimiva 3140 |
. . 3
β’ (π β π β βπ β Ο ((rank β ((πβπ)βπ)) β π« On β§ dom OrdIso( E ,
(rank β ((πβπ)βπ))) β βͺ ran
π»)) |
59 | | eqid 2733 |
. . . 4
β’ OrdIso( E
, βͺ π β Ο (rank β ((πβπ)βπ))) = OrdIso( E , βͺ π β Ο (rank β ((πβπ)βπ))) |
60 | 42, 59 | hsmexlem3 10372 |
. . 3
β’
(((Ο βΌ* Ο β§ βͺ ran π» β On) β§ βπ β Ο ((rank β ((πβπ)βπ)) β π« On β§ dom OrdIso( E ,
(rank β ((πβπ)βπ))) β βͺ ran
π»)) β dom OrdIso( E ,
βͺ π β Ο (rank β ((πβπ)βπ))) β (harβπ« (Ο
Γ βͺ ran π»))) |
61 | 27, 39, 58, 60 | syl21anc 837 |
. 2
β’ (π β π β dom OrdIso( E , βͺ π β Ο (rank β ((πβπ)βπ))) β (harβπ« (Ο
Γ βͺ ran π»))) |
62 | 24, 61 | eqeltrd 2834 |
1
β’ (π β π β (rankβπ) β (harβπ« (Ο
Γ βͺ ran π»))) |