Step | Hyp | Ref
| Expression |
1 | | fvex 6859 |
. . . 4
β’ (πΊβπ΄) β V |
2 | 1 | rnex 7853 |
. . 3
β’ ran
(πΊβπ΄) β V |
3 | | ssid 3970 |
. . . . 5
β’ π΄ β π΄ |
4 | | dfac12.1 |
. . . . . 6
β’ (π β π΄ β On) |
5 | | sseq1 3973 |
. . . . . . . . 9
β’ (π = π β (π β π΄ β π β π΄)) |
6 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π = π β (πΊβπ) = (πΊβπ)) |
7 | | f1eq1 6737 |
. . . . . . . . . . 11
β’ ((πΊβπ) = (πΊβπ) β ((πΊβπ):(π
1βπ)β1-1βOn β (πΊβπ):(π
1βπ)β1-1βOn)) |
8 | 6, 7 | syl 17 |
. . . . . . . . . 10
β’ (π = π β ((πΊβπ):(π
1βπ)β1-1βOn β (πΊβπ):(π
1βπ)β1-1βOn)) |
9 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π = π β (π
1βπ) =
(π
1βπ)) |
10 | | f1eq2 6738 |
. . . . . . . . . . 11
β’
((π
1βπ) = (π
1βπ) β ((πΊβπ):(π
1βπ)β1-1βOn β (πΊβπ):(π
1βπ)β1-1βOn)) |
11 | 9, 10 | syl 17 |
. . . . . . . . . 10
β’ (π = π β ((πΊβπ):(π
1βπ)β1-1βOn β (πΊβπ):(π
1βπ)β1-1βOn)) |
12 | 8, 11 | bitrd 279 |
. . . . . . . . 9
β’ (π = π β ((πΊβπ):(π
1βπ)β1-1βOn β (πΊβπ):(π
1βπ)β1-1βOn)) |
13 | 5, 12 | imbi12d 345 |
. . . . . . . 8
β’ (π = π β ((π β π΄ β (πΊβπ):(π
1βπ)β1-1βOn) β (π β π΄ β (πΊβπ):(π
1βπ)β1-1βOn))) |
14 | 13 | imbi2d 341 |
. . . . . . 7
β’ (π = π β ((π β (π β π΄ β (πΊβπ):(π
1βπ)β1-1βOn)) β (π β (π β π΄ β (πΊβπ):(π
1βπ)β1-1βOn)))) |
15 | | sseq1 3973 |
. . . . . . . . 9
β’ (π = π΄ β (π β π΄ β π΄ β π΄)) |
16 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π = π΄ β (πΊβπ) = (πΊβπ΄)) |
17 | | f1eq1 6737 |
. . . . . . . . . . 11
β’ ((πΊβπ) = (πΊβπ΄) β ((πΊβπ):(π
1βπ)β1-1βOn β (πΊβπ΄):(π
1βπ)β1-1βOn)) |
18 | 16, 17 | syl 17 |
. . . . . . . . . 10
β’ (π = π΄ β ((πΊβπ):(π
1βπ)β1-1βOn β (πΊβπ΄):(π
1βπ)β1-1βOn)) |
19 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π = π΄ β (π
1βπ) =
(π
1βπ΄)) |
20 | | f1eq2 6738 |
. . . . . . . . . . 11
β’
((π
1βπ) = (π
1βπ΄) β ((πΊβπ΄):(π
1βπ)β1-1βOn β (πΊβπ΄):(π
1βπ΄)β1-1βOn)) |
21 | 19, 20 | syl 17 |
. . . . . . . . . 10
β’ (π = π΄ β ((πΊβπ΄):(π
1βπ)β1-1βOn β (πΊβπ΄):(π
1βπ΄)β1-1βOn)) |
22 | 18, 21 | bitrd 279 |
. . . . . . . . 9
β’ (π = π΄ β ((πΊβπ):(π
1βπ)β1-1βOn β (πΊβπ΄):(π
1βπ΄)β1-1βOn)) |
23 | 15, 22 | imbi12d 345 |
. . . . . . . 8
β’ (π = π΄ β ((π β π΄ β (πΊβπ):(π
1βπ)β1-1βOn) β (π΄ β π΄ β (πΊβπ΄):(π
1βπ΄)β1-1βOn))) |
24 | 23 | imbi2d 341 |
. . . . . . 7
β’ (π = π΄ β ((π β (π β π΄ β (πΊβπ):(π
1βπ)β1-1βOn)) β (π β (π΄ β π΄ β (πΊβπ΄):(π
1βπ΄)β1-1βOn)))) |
25 | | r19.21v 3173 |
. . . . . . . 8
β’
(βπ β
π (π β (π β π΄ β (πΊβπ):(π
1βπ)β1-1βOn)) β (π β βπ β π (π β π΄ β (πΊβπ):(π
1βπ)β1-1βOn))) |
26 | | eloni 6331 |
. . . . . . . . . . . . . . . . . 18
β’ (π β On β Ord π) |
27 | 26 | ad2antrl 727 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β On β§ π β π΄)) β Ord π) |
28 | | ordelss 6337 |
. . . . . . . . . . . . . . . . 17
β’ ((Ord
π β§ π β π) β π β π) |
29 | 27, 28 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β On β§ π β π΄)) β§ π β π) β π β π) |
30 | | simplrr 777 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β On β§ π β π΄)) β§ π β π) β π β π΄) |
31 | 29, 30 | sstrd 3958 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β On β§ π β π΄)) β§ π β π) β π β π΄) |
32 | | pm5.5 362 |
. . . . . . . . . . . . . . 15
β’ (π β π΄ β ((π β π΄ β (πΊβπ):(π
1βπ)β1-1βOn) β (πΊβπ):(π
1βπ)β1-1βOn)) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β On β§ π β π΄)) β§ π β π) β ((π β π΄ β (πΊβπ):(π
1βπ)β1-1βOn) β (πΊβπ):(π
1βπ)β1-1βOn)) |
34 | 33 | ralbidva 3169 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β On β§ π β π΄)) β (βπ β π (π β π΄ β (πΊβπ):(π
1βπ)β1-1βOn) β βπ β π (πΊβπ):(π
1βπ)β1-1βOn)) |
35 | 4 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β On β§ π β π΄)) β§ βπ β π (πΊβπ):(π
1βπ)β1-1βOn) β π΄ β On) |
36 | | dfac12.3 |
. . . . . . . . . . . . . . . 16
β’ (π β πΉ:π«
(harβ(π
1βπ΄))β1-1βOn) |
37 | 36 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β On β§ π β π΄)) β§ βπ β π (πΊβπ):(π
1βπ)β1-1βOn) β πΉ:π«
(harβ(π
1βπ΄))β1-1βOn) |
38 | | dfac12.4 |
. . . . . . . . . . . . . . 15
β’ πΊ = recs((π₯ β V β¦ (π¦ β (π
1βdom
π₯) β¦ if(dom π₯ = βͺ
dom π₯, ((suc βͺ ran βͺ ran π₯ Β·o (rankβπ¦)) +o ((π₯βsuc (rankβπ¦))βπ¦)), (πΉβ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π¦)))))) |
39 | | simplrl 776 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β On β§ π β π΄)) β§ βπ β π (πΊβπ):(π
1βπ)β1-1βOn) β π β On) |
40 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ (β‘OrdIso( E , ran (πΊββͺ π)) β (πΊββͺ π)) = (β‘OrdIso( E , ran (πΊββͺ π)) β (πΊββͺ π)) |
41 | | simplrr 777 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β On β§ π β π΄)) β§ βπ β π (πΊβπ):(π
1βπ)β1-1βOn) β π β π΄) |
42 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β On β§ π β π΄)) β§ βπ β π (πΊβπ):(π
1βπ)β1-1βOn) β βπ β π (πΊβπ):(π
1βπ)β1-1βOn) |
43 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π§ β (πΊβπ) = (πΊβπ§)) |
44 | | f1eq1 6737 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΊβπ) = (πΊβπ§) β ((πΊβπ):(π
1βπ)β1-1βOn β (πΊβπ§):(π
1βπ)β1-1βOn)) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π§ β ((πΊβπ):(π
1βπ)β1-1βOn β (πΊβπ§):(π
1βπ)β1-1βOn)) |
46 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π§ β (π
1βπ) =
(π
1βπ§)) |
47 | | f1eq2 6738 |
. . . . . . . . . . . . . . . . . . 19
β’
((π
1βπ) = (π
1βπ§) β ((πΊβπ§):(π
1βπ)β1-1βOn β (πΊβπ§):(π
1βπ§)β1-1βOn)) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π§ β ((πΊβπ§):(π
1βπ)β1-1βOn β (πΊβπ§):(π
1βπ§)β1-1βOn)) |
49 | 45, 48 | bitrd 279 |
. . . . . . . . . . . . . . . . 17
β’ (π = π§ β ((πΊβπ):(π
1βπ)β1-1βOn β (πΊβπ§):(π
1βπ§)β1-1βOn)) |
50 | 49 | cbvralvw 3224 |
. . . . . . . . . . . . . . . 16
β’
(βπ β
π (πΊβπ):(π
1βπ)β1-1βOn β βπ§ β π (πΊβπ§):(π
1βπ§)β1-1βOn) |
51 | 42, 50 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β On β§ π β π΄)) β§ βπ β π (πΊβπ):(π
1βπ)β1-1βOn) β βπ§ β π (πΊβπ§):(π
1βπ§)β1-1βOn) |
52 | 35, 37, 38, 39, 40, 41, 51 | dfac12lem2 10088 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β On β§ π β π΄)) β§ βπ β π (πΊβπ):(π
1βπ)β1-1βOn) β (πΊβπ):(π
1βπ)β1-1βOn) |
53 | 52 | ex 414 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β On β§ π β π΄)) β (βπ β π (πΊβπ):(π
1βπ)β1-1βOn β (πΊβπ):(π
1βπ)β1-1βOn)) |
54 | 34, 53 | sylbid 239 |
. . . . . . . . . . . 12
β’ ((π β§ (π β On β§ π β π΄)) β (βπ β π (π β π΄ β (πΊβπ):(π
1βπ)β1-1βOn) β (πΊβπ):(π
1βπ)β1-1βOn)) |
55 | 54 | expr 458 |
. . . . . . . . . . 11
β’ ((π β§ π β On) β (π β π΄ β (βπ β π (π β π΄ β (πΊβπ):(π
1βπ)β1-1βOn) β (πΊβπ):(π
1βπ)β1-1βOn))) |
56 | 55 | com23 86 |
. . . . . . . . . 10
β’ ((π β§ π β On) β (βπ β π (π β π΄ β (πΊβπ):(π
1βπ)β1-1βOn) β (π β π΄ β (πΊβπ):(π
1βπ)β1-1βOn))) |
57 | 56 | expcom 415 |
. . . . . . . . 9
β’ (π β On β (π β (βπ β π (π β π΄ β (πΊβπ):(π
1βπ)β1-1βOn) β (π β π΄ β (πΊβπ):(π
1βπ)β1-1βOn)))) |
58 | 57 | a2d 29 |
. . . . . . . 8
β’ (π β On β ((π β βπ β π (π β π΄ β (πΊβπ):(π
1βπ)β1-1βOn)) β (π β (π β π΄ β (πΊβπ):(π
1βπ)β1-1βOn)))) |
59 | 25, 58 | biimtrid 241 |
. . . . . . 7
β’ (π β On β (βπ β π (π β (π β π΄ β (πΊβπ):(π
1βπ)β1-1βOn)) β (π β (π β π΄ β (πΊβπ):(π
1βπ)β1-1βOn)))) |
60 | 14, 24, 59 | tfis3 7798 |
. . . . . 6
β’ (π΄ β On β (π β (π΄ β π΄ β (πΊβπ΄):(π
1βπ΄)β1-1βOn))) |
61 | 4, 60 | mpcom 38 |
. . . . 5
β’ (π β (π΄ β π΄ β (πΊβπ΄):(π
1βπ΄)β1-1βOn)) |
62 | 3, 61 | mpi 20 |
. . . 4
β’ (π β (πΊβπ΄):(π
1βπ΄)β1-1βOn) |
63 | | f1f 6742 |
. . . 4
β’ ((πΊβπ΄):(π
1βπ΄)β1-1βOn β (πΊβπ΄):(π
1βπ΄)βΆOn) |
64 | | frn 6679 |
. . . 4
β’ ((πΊβπ΄):(π
1βπ΄)βΆOn β ran (πΊβπ΄) β On) |
65 | 62, 63, 64 | 3syl 18 |
. . 3
β’ (π β ran (πΊβπ΄) β On) |
66 | | onssnum 9984 |
. . 3
β’ ((ran
(πΊβπ΄) β V β§ ran (πΊβπ΄) β On) β ran (πΊβπ΄) β dom card) |
67 | 2, 65, 66 | sylancr 588 |
. 2
β’ (π β ran (πΊβπ΄) β dom card) |
68 | | f1f1orn 6799 |
. . . 4
β’ ((πΊβπ΄):(π
1βπ΄)β1-1βOn β (πΊβπ΄):(π
1βπ΄)β1-1-ontoβran
(πΊβπ΄)) |
69 | 62, 68 | syl 17 |
. . 3
β’ (π β (πΊβπ΄):(π
1βπ΄)β1-1-ontoβran
(πΊβπ΄)) |
70 | | fvex 6859 |
. . . 4
β’
(π
1βπ΄) β V |
71 | 70 | f1oen 8919 |
. . 3
β’ ((πΊβπ΄):(π
1βπ΄)β1-1-ontoβran
(πΊβπ΄) β (π
1βπ΄) β ran (πΊβπ΄)) |
72 | | ennum 9891 |
. . 3
β’
((π
1βπ΄) β ran (πΊβπ΄) β ((π
1βπ΄) β dom card β ran
(πΊβπ΄) β dom card)) |
73 | 69, 71, 72 | 3syl 18 |
. 2
β’ (π β
((π
1βπ΄) β dom card β ran (πΊβπ΄) β dom card)) |
74 | 67, 73 | mpbird 257 |
1
β’ (π β
(π
1βπ΄) β dom card) |