Step | Hyp | Ref
| Expression |
1 | | dfac12.4 |
. . . . . . . . . . . . . 14
β’ πΊ = recs((π₯ β V β¦ (π¦ β (π
1βdom
π₯) β¦ if(dom π₯ = βͺ
dom π₯, ((suc βͺ ran βͺ ran π₯ Β·o (rankβπ¦)) +o ((π₯βsuc (rankβπ¦))βπ¦)), (πΉβ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π¦)))))) |
2 | 1 | tfr1 8344 |
. . . . . . . . . . . . 13
β’ πΊ Fn On |
3 | | fnfun 6603 |
. . . . . . . . . . . . 13
β’ (πΊ Fn On β Fun πΊ) |
4 | 2, 3 | ax-mp 5 |
. . . . . . . . . . . 12
β’ Fun πΊ |
5 | | dfac12.5 |
. . . . . . . . . . . 12
β’ (π β πΆ β On) |
6 | | funimaexg 6588 |
. . . . . . . . . . . 12
β’ ((Fun
πΊ β§ πΆ β On) β (πΊ β πΆ) β V) |
7 | 4, 5, 6 | sylancr 588 |
. . . . . . . . . . 11
β’ (π β (πΊ β πΆ) β V) |
8 | | uniexg 7678 |
. . . . . . . . . . 11
β’ ((πΊ β πΆ) β V β βͺ (πΊ
β πΆ) β
V) |
9 | | rnexg 7842 |
. . . . . . . . . . 11
β’ (βͺ (πΊ
β πΆ) β V β
ran βͺ (πΊ β πΆ) β V) |
10 | 7, 8, 9 | 3syl 18 |
. . . . . . . . . 10
β’ (π β ran βͺ (πΊ
β πΆ) β
V) |
11 | | dfac12.8 |
. . . . . . . . . . . . . . 15
β’ (π β βπ§ β πΆ (πΊβπ§):(π
1βπ§)β1-1βOn) |
12 | | f1f 6739 |
. . . . . . . . . . . . . . . . 17
β’ ((πΊβπ§):(π
1βπ§)β1-1βOn β (πΊβπ§):(π
1βπ§)βΆOn) |
13 | | fssxp 6697 |
. . . . . . . . . . . . . . . . 17
β’ ((πΊβπ§):(π
1βπ§)βΆOn β (πΊβπ§) β ((π
1βπ§) Γ On)) |
14 | | ssv 3969 |
. . . . . . . . . . . . . . . . . . . 20
β’
(π
1βπ§) β V |
15 | | xpss1 5653 |
. . . . . . . . . . . . . . . . . . . 20
β’
((π
1βπ§) β V β
((π
1βπ§) Γ On) β (V Γ
On)) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
β’
((π
1βπ§) Γ On) β (V Γ
On) |
17 | | sstr 3953 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΊβπ§) β ((π
1βπ§) Γ On) β§
((π
1βπ§) Γ On) β (V Γ On)) β
(πΊβπ§) β (V Γ On)) |
18 | 16, 17 | mpan2 690 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΊβπ§) β ((π
1βπ§) Γ On) β (πΊβπ§) β (V Γ On)) |
19 | | fvex 6856 |
. . . . . . . . . . . . . . . . . . 19
β’ (πΊβπ§) β V |
20 | 19 | elpw 4565 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΊβπ§) β π« (V Γ On) β
(πΊβπ§) β (V Γ On)) |
21 | 18, 20 | sylibr 233 |
. . . . . . . . . . . . . . . . 17
β’ ((πΊβπ§) β ((π
1βπ§) Γ On) β (πΊβπ§) β π« (V Γ
On)) |
22 | 12, 13, 21 | 3syl 18 |
. . . . . . . . . . . . . . . 16
β’ ((πΊβπ§):(π
1βπ§)β1-1βOn β (πΊβπ§) β π« (V Γ
On)) |
23 | 22 | ralimi 3087 |
. . . . . . . . . . . . . . 15
β’
(βπ§ β
πΆ (πΊβπ§):(π
1βπ§)β1-1βOn β βπ§ β πΆ (πΊβπ§) β π« (V Γ
On)) |
24 | 11, 23 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β βπ§ β πΆ (πΊβπ§) β π« (V Γ
On)) |
25 | | onss 7720 |
. . . . . . . . . . . . . . . . 17
β’ (πΆ β On β πΆ β On) |
26 | 5, 25 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β πΆ β On) |
27 | 2 | fndmi 6607 |
. . . . . . . . . . . . . . . 16
β’ dom πΊ = On |
28 | 26, 27 | sseqtrrdi 3996 |
. . . . . . . . . . . . . . 15
β’ (π β πΆ β dom πΊ) |
29 | | funimass4 6908 |
. . . . . . . . . . . . . . 15
β’ ((Fun
πΊ β§ πΆ β dom πΊ) β ((πΊ β πΆ) β π« (V Γ On) β
βπ§ β πΆ (πΊβπ§) β π« (V Γ
On))) |
30 | 4, 28, 29 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ (π β ((πΊ β πΆ) β π« (V Γ On) β
βπ§ β πΆ (πΊβπ§) β π« (V Γ
On))) |
31 | 24, 30 | mpbird 257 |
. . . . . . . . . . . . 13
β’ (π β (πΊ β πΆ) β π« (V Γ
On)) |
32 | | sspwuni 5061 |
. . . . . . . . . . . . 13
β’ ((πΊ β πΆ) β π« (V Γ On) β
βͺ (πΊ β πΆ) β (V Γ On)) |
33 | 31, 32 | sylib 217 |
. . . . . . . . . . . 12
β’ (π β βͺ (πΊ
β πΆ) β (V
Γ On)) |
34 | | rnss 5895 |
. . . . . . . . . . . 12
β’ (βͺ (πΊ
β πΆ) β (V
Γ On) β ran βͺ (πΊ β πΆ) β ran (V Γ
On)) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . 11
β’ (π β ran βͺ (πΊ
β πΆ) β ran (V
Γ On)) |
36 | | rnxpss 6125 |
. . . . . . . . . . 11
β’ ran (V
Γ On) β On |
37 | 35, 36 | sstrdi 3957 |
. . . . . . . . . 10
β’ (π β ran βͺ (πΊ
β πΆ) β
On) |
38 | | ssonuni 7715 |
. . . . . . . . . 10
β’ (ran
βͺ (πΊ β πΆ) β V β (ran βͺ (πΊ
β πΆ) β On
β βͺ ran βͺ (πΊ β πΆ) β On)) |
39 | 10, 37, 38 | sylc 65 |
. . . . . . . . 9
β’ (π β βͺ ran βͺ (πΊ β πΆ) β On) |
40 | | onsuc 7747 |
. . . . . . . . 9
β’ (βͺ ran βͺ (πΊ β πΆ) β On β suc βͺ ran βͺ (πΊ β πΆ) β On) |
41 | 39, 40 | syl 17 |
. . . . . . . 8
β’ (π β suc βͺ ran βͺ (πΊ β πΆ) β On) |
42 | 41 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β suc βͺ ran βͺ (πΊ β πΆ) β On) |
43 | | rankon 9732 |
. . . . . . 7
β’
(rankβπ¦)
β On |
44 | | omcl 8483 |
. . . . . . 7
β’ ((suc
βͺ ran βͺ (πΊ β πΆ) β On β§ (rankβπ¦) β On) β (suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) β On) |
45 | 42, 43, 44 | sylancl 587 |
. . . . . 6
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β (suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) β On) |
46 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π§ = suc (rankβπ¦) β (πΊβπ§) = (πΊβsuc (rankβπ¦))) |
47 | | f1eq1 6734 |
. . . . . . . . . . 11
β’ ((πΊβπ§) = (πΊβsuc (rankβπ¦)) β ((πΊβπ§):(π
1βπ§)β1-1βOn β (πΊβsuc (rankβπ¦)):(π
1βπ§)β1-1βOn)) |
48 | 46, 47 | syl 17 |
. . . . . . . . . 10
β’ (π§ = suc (rankβπ¦) β ((πΊβπ§):(π
1βπ§)β1-1βOn β (πΊβsuc (rankβπ¦)):(π
1βπ§)β1-1βOn)) |
49 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π§ = suc (rankβπ¦) β
(π
1βπ§) = (π
1βsuc
(rankβπ¦))) |
50 | | f1eq2 6735 |
. . . . . . . . . . 11
β’
((π
1βπ§) = (π
1βsuc
(rankβπ¦)) β
((πΊβsuc
(rankβπ¦)):(π
1βπ§)β1-1βOn β (πΊβsuc (rankβπ¦)):(π
1βsuc
(rankβπ¦))β1-1βOn)) |
51 | 49, 50 | syl 17 |
. . . . . . . . . 10
β’ (π§ = suc (rankβπ¦) β ((πΊβsuc (rankβπ¦)):(π
1βπ§)β1-1βOn β (πΊβsuc (rankβπ¦)):(π
1βsuc
(rankβπ¦))β1-1βOn)) |
52 | 48, 51 | bitrd 279 |
. . . . . . . . 9
β’ (π§ = suc (rankβπ¦) β ((πΊβπ§):(π
1βπ§)β1-1βOn β (πΊβsuc (rankβπ¦)):(π
1βsuc
(rankβπ¦))β1-1βOn)) |
53 | 11 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β βπ§ β πΆ (πΊβπ§):(π
1βπ§)β1-1βOn) |
54 | | rankr1ai 9735 |
. . . . . . . . . . . 12
β’ (π¦ β
(π
1βπΆ) β (rankβπ¦) β πΆ) |
55 | 54 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β (rankβπ¦) β πΆ) |
56 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β πΆ = βͺ πΆ) |
57 | 55, 56 | eleqtrd 2840 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β (rankβπ¦) β βͺ πΆ) |
58 | | eloni 6328 |
. . . . . . . . . . . . 13
β’ (πΆ β On β Ord πΆ) |
59 | 5, 58 | syl 17 |
. . . . . . . . . . . 12
β’ (π β Ord πΆ) |
60 | 59 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β Ord πΆ) |
61 | | ordsucuniel 7760 |
. . . . . . . . . . 11
β’ (Ord
πΆ β ((rankβπ¦) β βͺ πΆ
β suc (rankβπ¦)
β πΆ)) |
62 | 60, 61 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β ((rankβπ¦) β βͺ πΆ
β suc (rankβπ¦)
β πΆ)) |
63 | 57, 62 | mpbid 231 |
. . . . . . . . 9
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β suc (rankβπ¦) β πΆ) |
64 | 52, 53, 63 | rspcdva 3583 |
. . . . . . . 8
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β (πΊβsuc (rankβπ¦)):(π
1βsuc
(rankβπ¦))β1-1βOn) |
65 | | f1f 6739 |
. . . . . . . 8
β’ ((πΊβsuc (rankβπ¦)):(π
1βsuc
(rankβπ¦))β1-1βOn β (πΊβsuc (rankβπ¦)):(π
1βsuc
(rankβπ¦))βΆOn) |
66 | 64, 65 | syl 17 |
. . . . . . 7
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β (πΊβsuc (rankβπ¦)):(π
1βsuc
(rankβπ¦))βΆOn) |
67 | | r1elwf 9733 |
. . . . . . . . 9
β’ (π¦ β
(π
1βπΆ) β π¦ β βͺ
(π
1 β On)) |
68 | 67 | ad2antlr 726 |
. . . . . . . 8
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β π¦ β βͺ
(π
1 β On)) |
69 | | rankidb 9737 |
. . . . . . . 8
β’ (π¦ β βͺ (π
1 β On) β π¦ β
(π
1βsuc (rankβπ¦))) |
70 | 68, 69 | syl 17 |
. . . . . . 7
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β π¦ β (π
1βsuc
(rankβπ¦))) |
71 | 66, 70 | ffvelcdmd 7037 |
. . . . . 6
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β ((πΊβsuc (rankβπ¦))βπ¦) β On) |
72 | | oacl 8482 |
. . . . . 6
β’ (((suc
βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) β On β§ ((πΊβsuc (rankβπ¦))βπ¦) β On) β ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)) β On) |
73 | 45, 71, 72 | syl2anc 585 |
. . . . 5
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)) β On) |
74 | | dfac12.3 |
. . . . . . . 8
β’ (π β πΉ:π«
(harβ(π
1βπ΄))β1-1βOn) |
75 | | f1f 6739 |
. . . . . . . 8
β’ (πΉ:π«
(harβ(π
1βπ΄))β1-1βOn β πΉ:π«
(harβ(π
1βπ΄))βΆOn) |
76 | 74, 75 | syl 17 |
. . . . . . 7
β’ (π β πΉ:π«
(harβ(π
1βπ΄))βΆOn) |
77 | 76 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β πΉ:π«
(harβ(π
1βπ΄))βΆOn) |
78 | | imassrn 6025 |
. . . . . . . 8
β’ (π» β π¦) β ran π» |
79 | | fvex 6856 |
. . . . . . . . . . . . . . 15
β’ (πΊββͺ πΆ)
β V |
80 | 79 | rnex 7850 |
. . . . . . . . . . . . . 14
β’ ran
(πΊββͺ πΆ)
β V |
81 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ = βͺ
πΆ β (πΊβπ§) = (πΊββͺ πΆ)) |
82 | | f1eq1 6734 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΊβπ§) = (πΊββͺ πΆ) β ((πΊβπ§):(π
1βπ§)β1-1βOn β (πΊββͺ πΆ):(π
1βπ§)β1-1βOn)) |
83 | 81, 82 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ = βͺ
πΆ β ((πΊβπ§):(π
1βπ§)β1-1βOn β (πΊββͺ πΆ):(π
1βπ§)β1-1βOn)) |
84 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ = βͺ
πΆ β
(π
1βπ§) = (π
1ββͺ πΆ)) |
85 | | f1eq2 6735 |
. . . . . . . . . . . . . . . . . . 19
β’
((π
1βπ§) = (π
1ββͺ πΆ)
β ((πΊββͺ πΆ):(π
1βπ§)β1-1βOn β (πΊββͺ πΆ):(π
1ββͺ πΆ)β1-1βOn)) |
86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ = βͺ
πΆ β ((πΊββͺ πΆ):(π
1βπ§)β1-1βOn β (πΊββͺ πΆ):(π
1ββͺ πΆ)β1-1βOn)) |
87 | 83, 86 | bitrd 279 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = βͺ
πΆ β ((πΊβπ§):(π
1βπ§)β1-1βOn β (πΊββͺ πΆ):(π
1ββͺ πΆ)β1-1βOn)) |
88 | 11 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β βπ§ β πΆ (πΊβπ§):(π
1βπ§)β1-1βOn) |
89 | 5 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β πΆ β On) |
90 | | onuni 7724 |
. . . . . . . . . . . . . . . . . . 19
β’ (πΆ β On β βͺ πΆ
β On) |
91 | | sucidg 6399 |
. . . . . . . . . . . . . . . . . . 19
β’ (βͺ πΆ
β On β βͺ πΆ β suc βͺ
πΆ) |
92 | 89, 90, 91 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β βͺ πΆ
β suc βͺ πΆ) |
93 | 59 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π¦ β (π
1βπΆ)) β Ord πΆ) |
94 | | orduniorsuc 7766 |
. . . . . . . . . . . . . . . . . . . 20
β’ (Ord
πΆ β (πΆ = βͺ πΆ β¨ πΆ = suc βͺ πΆ)) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π¦ β (π
1βπΆ)) β (πΆ = βͺ πΆ β¨ πΆ = suc βͺ πΆ)) |
96 | 95 | orcanai 1002 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β πΆ = suc βͺ πΆ) |
97 | 92, 96 | eleqtrrd 2841 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β βͺ πΆ
β πΆ) |
98 | 87, 88, 97 | rspcdva 3583 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β (πΊββͺ πΆ):(π
1ββͺ πΆ)β1-1βOn) |
99 | | f1f 6739 |
. . . . . . . . . . . . . . . 16
β’ ((πΊββͺ πΆ):(π
1ββͺ πΆ)β1-1βOn β (πΊββͺ πΆ):(π
1ββͺ πΆ)βΆOn) |
100 | | frn 6676 |
. . . . . . . . . . . . . . . 16
β’ ((πΊββͺ πΆ):(π
1ββͺ πΆ)βΆOn β ran (πΊββͺ πΆ) β On) |
101 | 98, 99, 100 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β ran (πΊββͺ πΆ) β On) |
102 | | epweon 7710 |
. . . . . . . . . . . . . . 15
β’ E We
On |
103 | | wess 5621 |
. . . . . . . . . . . . . . 15
β’ (ran
(πΊββͺ πΆ)
β On β ( E We On β E We ran (πΊββͺ πΆ))) |
104 | 101, 102,
103 | mpisyl 21 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β E We ran (πΊββͺ πΆ)) |
105 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’ OrdIso( E
, ran (πΊββͺ πΆ))
= OrdIso( E , ran (πΊββͺ πΆ)) |
106 | 105 | oiiso 9474 |
. . . . . . . . . . . . . 14
β’ ((ran
(πΊββͺ πΆ)
β V β§ E We ran (πΊββͺ πΆ)) β OrdIso( E , ran (πΊββͺ πΆ))
Isom E , E (dom OrdIso( E , ran (πΊββͺ πΆ)), ran (πΊββͺ πΆ))) |
107 | 80, 104, 106 | sylancr 588 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β OrdIso( E , ran (πΊββͺ πΆ))
Isom E , E (dom OrdIso( E , ran (πΊββͺ πΆ)), ran (πΊββͺ πΆ))) |
108 | | isof1o 7269 |
. . . . . . . . . . . . 13
β’ (OrdIso(
E , ran (πΊββͺ πΆ))
Isom E , E (dom OrdIso( E , ran (πΊββͺ πΆ)), ran (πΊββͺ πΆ)) β OrdIso( E , ran (πΊββͺ πΆ)):dom OrdIso( E , ran (πΊββͺ πΆ))β1-1-ontoβran
(πΊββͺ πΆ)) |
109 | | f1ocnv 6797 |
. . . . . . . . . . . . 13
β’ (OrdIso(
E , ran (πΊββͺ πΆ)):dom OrdIso( E , ran (πΊββͺ πΆ))β1-1-ontoβran
(πΊββͺ πΆ)
β β‘OrdIso( E , ran (πΊββͺ πΆ)):ran (πΊββͺ πΆ)β1-1-ontoβdom
OrdIso( E , ran (πΊββͺ πΆ))) |
110 | | f1of1 6784 |
. . . . . . . . . . . . 13
β’ (β‘OrdIso( E , ran (πΊββͺ πΆ)):ran (πΊββͺ πΆ)β1-1-ontoβdom
OrdIso( E , ran (πΊββͺ πΆ)) β β‘OrdIso( E , ran (πΊββͺ πΆ)):ran (πΊββͺ πΆ)β1-1βdom OrdIso( E , ran (πΊββͺ πΆ))) |
111 | 107, 108,
109, 110 | 4syl 19 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β β‘OrdIso( E , ran (πΊββͺ πΆ)):ran (πΊββͺ πΆ)β1-1βdom OrdIso( E , ran (πΊββͺ πΆ))) |
112 | | f1f1orn 6796 |
. . . . . . . . . . . . 13
β’ ((πΊββͺ πΆ):(π
1ββͺ πΆ)β1-1βOn β (πΊββͺ πΆ):(π
1ββͺ πΆ)β1-1-ontoβran
(πΊββͺ πΆ)) |
113 | | f1of1 6784 |
. . . . . . . . . . . . 13
β’ ((πΊββͺ πΆ):(π
1ββͺ πΆ)β1-1-ontoβran
(πΊββͺ πΆ)
β (πΊββͺ πΆ):(π
1ββͺ πΆ)β1-1βran (πΊββͺ πΆ)) |
114 | 98, 112, 113 | 3syl 18 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β (πΊββͺ πΆ):(π
1ββͺ πΆ)β1-1βran (πΊββͺ πΆ)) |
115 | | f1co 6751 |
. . . . . . . . . . . 12
β’ ((β‘OrdIso( E , ran (πΊββͺ πΆ)):ran (πΊββͺ πΆ)β1-1βdom OrdIso( E , ran (πΊββͺ πΆ)) β§ (πΊββͺ πΆ):(π
1ββͺ πΆ)β1-1βran (πΊββͺ πΆ)) β (β‘OrdIso( E , ran (πΊββͺ πΆ)) β (πΊββͺ πΆ)):(π
1ββͺ πΆ)β1-1βdom OrdIso( E , ran (πΊββͺ πΆ))) |
116 | 111, 114,
115 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β (β‘OrdIso( E , ran (πΊββͺ πΆ)) β (πΊββͺ πΆ)):(π
1ββͺ πΆ)β1-1βdom OrdIso( E , ran (πΊββͺ πΆ))) |
117 | | dfac12.h |
. . . . . . . . . . . 12
β’ π» = (β‘OrdIso( E , ran (πΊββͺ πΆ)) β (πΊββͺ πΆ)) |
118 | | f1eq1 6734 |
. . . . . . . . . . . 12
β’ (π» = (β‘OrdIso( E , ran (πΊββͺ πΆ)) β (πΊββͺ πΆ)) β (π»:(π
1ββͺ πΆ)β1-1βdom OrdIso( E , ran (πΊββͺ πΆ)) β (β‘OrdIso( E , ran (πΊββͺ πΆ)) β (πΊββͺ πΆ)):(π
1ββͺ πΆ)β1-1βdom OrdIso( E , ran (πΊββͺ πΆ)))) |
119 | 117, 118 | ax-mp 5 |
. . . . . . . . . . 11
β’ (π»:(π
1ββͺ πΆ)β1-1βdom OrdIso( E , ran (πΊββͺ πΆ)) β (β‘OrdIso( E , ran (πΊββͺ πΆ)) β (πΊββͺ πΆ)):(π
1ββͺ πΆ)β1-1βdom OrdIso( E , ran (πΊββͺ πΆ))) |
120 | 116, 119 | sylibr 233 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β π»:(π
1ββͺ πΆ)β1-1βdom OrdIso( E , ran (πΊββͺ πΆ))) |
121 | | f1f 6739 |
. . . . . . . . . 10
β’ (π»:(π
1ββͺ πΆ)β1-1βdom OrdIso( E , ran (πΊββͺ πΆ)) β π»:(π
1ββͺ πΆ)βΆdom OrdIso( E , ran (πΊββͺ πΆ))) |
122 | | frn 6676 |
. . . . . . . . . 10
β’ (π»:(π
1ββͺ πΆ)βΆdom OrdIso( E , ran (πΊββͺ πΆ))
β ran π» β dom
OrdIso( E , ran (πΊββͺ πΆ))) |
123 | 120, 121,
122 | 3syl 18 |
. . . . . . . . 9
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β ran π» β dom OrdIso( E , ran (πΊββͺ πΆ))) |
124 | | harcl 9496 |
. . . . . . . . . . 11
β’
(harβ(π
1βπ΄)) β On |
125 | 124 | onordi 6429 |
. . . . . . . . . 10
β’ Ord
(harβ(π
1βπ΄)) |
126 | 105 | oion 9473 |
. . . . . . . . . . . 12
β’ (ran
(πΊββͺ πΆ)
β V β dom OrdIso( E , ran (πΊββͺ πΆ)) β On) |
127 | 80, 126 | mp1i 13 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β dom OrdIso( E , ran
(πΊββͺ πΆ))
β On) |
128 | 105 | oien 9475 |
. . . . . . . . . . . . 13
β’ ((ran
(πΊββͺ πΆ)
β V β§ E We ran (πΊββͺ πΆ)) β dom OrdIso( E , ran
(πΊββͺ πΆ))
β ran (πΊββͺ πΆ)) |
129 | 80, 104, 128 | sylancr 588 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β dom OrdIso( E , ran
(πΊββͺ πΆ))
β ran (πΊββͺ πΆ)) |
130 | | fvex 6856 |
. . . . . . . . . . . . . . 15
β’
(π
1ββͺ πΆ) β V |
131 | 130 | f1oen 8914 |
. . . . . . . . . . . . . 14
β’ ((πΊββͺ πΆ):(π
1ββͺ πΆ)β1-1-ontoβran
(πΊββͺ πΆ)
β (π
1ββͺ πΆ) β ran (πΊββͺ πΆ)) |
132 | | ensym 8944 |
. . . . . . . . . . . . . 14
β’
((π
1ββͺ πΆ) β ran (πΊββͺ πΆ) β ran (πΊββͺ πΆ) β
(π
1ββͺ πΆ)) |
133 | 98, 112, 131, 132 | 4syl 19 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β ran (πΊββͺ πΆ) β
(π
1ββͺ πΆ)) |
134 | | fvex 6856 |
. . . . . . . . . . . . . 14
β’
(π
1βπ΄) β V |
135 | | dfac12.1 |
. . . . . . . . . . . . . . . 16
β’ (π β π΄ β On) |
136 | 135 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β π΄ β On) |
137 | | dfac12.6 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΆ β π΄) |
138 | 137 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β πΆ β π΄) |
139 | 138, 97 | sseldd 3946 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β βͺ πΆ
β π΄) |
140 | | r1ord2 9718 |
. . . . . . . . . . . . . . 15
β’ (π΄ β On β (βͺ πΆ
β π΄ β
(π
1ββͺ πΆ) β (π
1βπ΄))) |
141 | 136, 139,
140 | sylc 65 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β
(π
1ββͺ πΆ) β (π
1βπ΄)) |
142 | | ssdomg 8941 |
. . . . . . . . . . . . . 14
β’
((π
1βπ΄) β V β
((π
1ββͺ πΆ) β (π
1βπ΄) β
(π
1ββͺ πΆ) βΌ (π
1βπ΄))) |
143 | 134, 141,
142 | mpsyl 68 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β
(π
1ββͺ πΆ) βΌ (π
1βπ΄)) |
144 | | endomtr 8953 |
. . . . . . . . . . . . 13
β’ ((ran
(πΊββͺ πΆ)
β (π
1ββͺ πΆ) β§
(π
1ββͺ πΆ) βΌ (π
1βπ΄)) β ran (πΊββͺ πΆ) βΌ
(π
1βπ΄)) |
145 | 133, 143,
144 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β ran (πΊββͺ πΆ) βΌ
(π
1βπ΄)) |
146 | | endomtr 8953 |
. . . . . . . . . . . 12
β’ ((dom
OrdIso( E , ran (πΊββͺ πΆ)) β ran (πΊββͺ πΆ)
β§ ran (πΊββͺ πΆ)
βΌ (π
1βπ΄)) β dom OrdIso( E , ran (πΊββͺ πΆ))
βΌ (π
1βπ΄)) |
147 | 129, 145,
146 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β dom OrdIso( E , ran
(πΊββͺ πΆ))
βΌ (π
1βπ΄)) |
148 | | elharval 9498 |
. . . . . . . . . . 11
β’ (dom
OrdIso( E , ran (πΊββͺ πΆ)) β
(harβ(π
1βπ΄)) β (dom OrdIso( E , ran (πΊββͺ πΆ))
β On β§ dom OrdIso( E , ran (πΊββͺ πΆ)) βΌ
(π
1βπ΄))) |
149 | 127, 147,
148 | sylanbrc 584 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β dom OrdIso( E , ran
(πΊββͺ πΆ))
β (harβ(π
1βπ΄))) |
150 | | ordelss 6334 |
. . . . . . . . . 10
β’ ((Ord
(harβ(π
1βπ΄)) β§ dom OrdIso( E , ran (πΊββͺ πΆ))
β (harβ(π
1βπ΄))) β dom OrdIso( E , ran (πΊββͺ πΆ))
β (harβ(π
1βπ΄))) |
151 | 125, 149,
150 | sylancr 588 |
. . . . . . . . 9
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β dom OrdIso( E , ran
(πΊββͺ πΆ))
β (harβ(π
1βπ΄))) |
152 | 123, 151 | sstrd 3955 |
. . . . . . . 8
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β ran π» β
(harβ(π
1βπ΄))) |
153 | 78, 152 | sstrid 3956 |
. . . . . . 7
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β (π» β π¦) β
(harβ(π
1βπ΄))) |
154 | | fvex 6856 |
. . . . . . . 8
β’
(harβ(π
1βπ΄)) β V |
155 | 154 | elpw2 5303 |
. . . . . . 7
β’ ((π» β π¦) β π«
(harβ(π
1βπ΄)) β (π» β π¦) β
(harβ(π
1βπ΄))) |
156 | 153, 155 | sylibr 233 |
. . . . . 6
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β (π» β π¦) β π«
(harβ(π
1βπ΄))) |
157 | 77, 156 | ffvelcdmd 7037 |
. . . . 5
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β (πΉβ(π» β π¦)) β On) |
158 | 73, 157 | ifclda 4522 |
. . . 4
β’ ((π β§ π¦ β (π
1βπΆ)) β if(πΆ = βͺ πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)), (πΉβ(π» β π¦))) β On) |
159 | 158 | ex 414 |
. . 3
β’ (π β (π¦ β (π
1βπΆ) β if(πΆ = βͺ πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)), (πΉβ(π» β π¦))) β On)) |
160 | | iftrue 4493 |
. . . . . . . 8
β’ (πΆ = βͺ
πΆ β if(πΆ = βͺ
πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)), (πΉβ(π» β π¦))) = ((suc βͺ ran
βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦))) |
161 | | iftrue 4493 |
. . . . . . . 8
β’ (πΆ = βͺ
πΆ β if(πΆ = βͺ
πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ§)) +o ((πΊβsuc (rankβπ§))βπ§)), (πΉβ(π» β π§))) = ((suc βͺ ran
βͺ (πΊ β πΆ) Β·o (rankβπ§)) +o ((πΊβsuc (rankβπ§))βπ§))) |
162 | 160, 161 | eqeq12d 2753 |
. . . . . . 7
β’ (πΆ = βͺ
πΆ β (if(πΆ = βͺ
πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)), (πΉβ(π» β π¦))) = if(πΆ = βͺ πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ§)) +o ((πΊβsuc (rankβπ§))βπ§)), (πΉβ(π» β π§))) β ((suc βͺ
ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)) = ((suc βͺ ran
βͺ (πΊ β πΆ) Β·o (rankβπ§)) +o ((πΊβsuc (rankβπ§))βπ§)))) |
163 | 162 | adantl 483 |
. . . . . 6
β’ (((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ πΆ = βͺ πΆ) β (if(πΆ = βͺ πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)), (πΉβ(π» β π¦))) = if(πΆ = βͺ πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ§)) +o ((πΊβsuc (rankβπ§))βπ§)), (πΉβ(π» β π§))) β ((suc βͺ
ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)) = ((suc βͺ ran
βͺ (πΊ β πΆ) Β·o (rankβπ§)) +o ((πΊβsuc (rankβπ§))βπ§)))) |
164 | 41 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ πΆ = βͺ πΆ) β suc βͺ ran βͺ (πΊ β πΆ) β On) |
165 | | nsuceq0 6401 |
. . . . . . . 8
β’ suc βͺ ran βͺ (πΊ β πΆ) β β
|
166 | 165 | a1i 11 |
. . . . . . 7
β’ (((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ πΆ = βͺ πΆ) β suc βͺ ran βͺ (πΊ β πΆ) β β
) |
167 | 43 | a1i 11 |
. . . . . . 7
β’ (((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ πΆ = βͺ πΆ) β (rankβπ¦) β On) |
168 | | onsucuni 7764 |
. . . . . . . . . . 11
β’ (ran
βͺ (πΊ β πΆ) β On β ran βͺ (πΊ
β πΆ) β suc
βͺ ran βͺ (πΊ β πΆ)) |
169 | 37, 168 | syl 17 |
. . . . . . . . . 10
β’ (π β ran βͺ (πΊ
β πΆ) β suc
βͺ ran βͺ (πΊ β πΆ)) |
170 | 169 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β ran βͺ (πΊ
β πΆ) β suc
βͺ ran βͺ (πΊ β πΆ)) |
171 | 26 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β πΆ β On) |
172 | | fnfvima 7184 |
. . . . . . . . . . . 12
β’ ((πΊ Fn On β§ πΆ β On β§ suc (rankβπ¦) β πΆ) β (πΊβsuc (rankβπ¦)) β (πΊ β πΆ)) |
173 | 2, 171, 63, 172 | mp3an2i 1467 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β (πΊβsuc (rankβπ¦)) β (πΊ β πΆ)) |
174 | | elssuni 4899 |
. . . . . . . . . . 11
β’ ((πΊβsuc (rankβπ¦)) β (πΊ β πΆ) β (πΊβsuc (rankβπ¦)) β βͺ
(πΊ β πΆ)) |
175 | | rnss 5895 |
. . . . . . . . . . 11
β’ ((πΊβsuc (rankβπ¦)) β βͺ (πΊ
β πΆ) β ran
(πΊβsuc
(rankβπ¦)) β ran
βͺ (πΊ β πΆ)) |
176 | 173, 174,
175 | 3syl 18 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β ran (πΊβsuc (rankβπ¦)) β ran βͺ
(πΊ β πΆ)) |
177 | | f1fn 6740 |
. . . . . . . . . . . 12
β’ ((πΊβsuc (rankβπ¦)):(π
1βsuc
(rankβπ¦))β1-1βOn β (πΊβsuc (rankβπ¦)) Fn (π
1βsuc
(rankβπ¦))) |
178 | 64, 177 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β (πΊβsuc (rankβπ¦)) Fn (π
1βsuc
(rankβπ¦))) |
179 | | fnfvelrn 7032 |
. . . . . . . . . . 11
β’ (((πΊβsuc (rankβπ¦)) Fn
(π
1βsuc (rankβπ¦)) β§ π¦ β (π
1βsuc
(rankβπ¦))) β
((πΊβsuc
(rankβπ¦))βπ¦) β ran (πΊβsuc (rankβπ¦))) |
180 | 178, 70, 179 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β ((πΊβsuc (rankβπ¦))βπ¦) β ran (πΊβsuc (rankβπ¦))) |
181 | 176, 180 | sseldd 3946 |
. . . . . . . . 9
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β ((πΊβsuc (rankβπ¦))βπ¦) β ran βͺ
(πΊ β πΆ)) |
182 | 170, 181 | sseldd 3946 |
. . . . . . . 8
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β ((πΊβsuc (rankβπ¦))βπ¦) β suc βͺ ran
βͺ (πΊ β πΆ)) |
183 | 182 | adantlrr 720 |
. . . . . . 7
β’ (((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ πΆ = βͺ πΆ) β ((πΊβsuc (rankβπ¦))βπ¦) β suc βͺ ran
βͺ (πΊ β πΆ)) |
184 | | rankon 9732 |
. . . . . . . 8
β’
(rankβπ§)
β On |
185 | 184 | a1i 11 |
. . . . . . 7
β’ (((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ πΆ = βͺ πΆ) β (rankβπ§) β On) |
186 | | eleq1w 2821 |
. . . . . . . . . . . 12
β’ (π¦ = π§ β (π¦ β (π
1βπΆ) β π§ β (π
1βπΆ))) |
187 | 186 | anbi2d 630 |
. . . . . . . . . . 11
β’ (π¦ = π§ β ((π β§ π¦ β (π
1βπΆ)) β (π β§ π§ β (π
1βπΆ)))) |
188 | 187 | anbi1d 631 |
. . . . . . . . . 10
β’ (π¦ = π§ β (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β ((π β§ π§ β (π
1βπΆ)) β§ πΆ = βͺ πΆ))) |
189 | | fveq2 6843 |
. . . . . . . . . . . . . 14
β’ (π¦ = π§ β (rankβπ¦) = (rankβπ§)) |
190 | | suceq 6384 |
. . . . . . . . . . . . . 14
β’
((rankβπ¦) =
(rankβπ§) β suc
(rankβπ¦) = suc
(rankβπ§)) |
191 | 189, 190 | syl 17 |
. . . . . . . . . . . . 13
β’ (π¦ = π§ β suc (rankβπ¦) = suc (rankβπ§)) |
192 | 191 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ (π¦ = π§ β (πΊβsuc (rankβπ¦)) = (πΊβsuc (rankβπ§))) |
193 | | id 22 |
. . . . . . . . . . . 12
β’ (π¦ = π§ β π¦ = π§) |
194 | 192, 193 | fveq12d 6850 |
. . . . . . . . . . 11
β’ (π¦ = π§ β ((πΊβsuc (rankβπ¦))βπ¦) = ((πΊβsuc (rankβπ§))βπ§)) |
195 | 194 | eleq1d 2823 |
. . . . . . . . . 10
β’ (π¦ = π§ β (((πΊβsuc (rankβπ¦))βπ¦) β suc βͺ ran
βͺ (πΊ β πΆ) β ((πΊβsuc (rankβπ§))βπ§) β suc βͺ ran
βͺ (πΊ β πΆ))) |
196 | 188, 195 | imbi12d 345 |
. . . . . . . . 9
β’ (π¦ = π§ β ((((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β ((πΊβsuc (rankβπ¦))βπ¦) β suc βͺ ran
βͺ (πΊ β πΆ)) β (((π β§ π§ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β ((πΊβsuc (rankβπ§))βπ§) β suc βͺ ran
βͺ (πΊ β πΆ)))) |
197 | 196, 182 | chvarvv 2003 |
. . . . . . . 8
β’ (((π β§ π§ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β ((πΊβsuc (rankβπ§))βπ§) β suc βͺ ran
βͺ (πΊ β πΆ)) |
198 | 197 | adantlrl 719 |
. . . . . . 7
β’ (((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ πΆ = βͺ πΆ) β ((πΊβsuc (rankβπ§))βπ§) β suc βͺ ran
βͺ (πΊ β πΆ)) |
199 | | omopth2 8532 |
. . . . . . 7
β’ (((suc
βͺ ran βͺ (πΊ β πΆ) β On β§ suc βͺ ran βͺ (πΊ β πΆ) β β
) β§ ((rankβπ¦) β On β§ ((πΊβsuc (rankβπ¦))βπ¦) β suc βͺ ran
βͺ (πΊ β πΆ)) β§ ((rankβπ§) β On β§ ((πΊβsuc (rankβπ§))βπ§) β suc βͺ ran
βͺ (πΊ β πΆ))) β (((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)) = ((suc βͺ ran
βͺ (πΊ β πΆ) Β·o (rankβπ§)) +o ((πΊβsuc (rankβπ§))βπ§)) β ((rankβπ¦) = (rankβπ§) β§ ((πΊβsuc (rankβπ¦))βπ¦) = ((πΊβsuc (rankβπ§))βπ§)))) |
200 | 164, 166,
167, 183, 185, 198, 199 | syl222anc 1387 |
. . . . . 6
β’ (((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ πΆ = βͺ πΆ) β (((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)) = ((suc βͺ ran
βͺ (πΊ β πΆ) Β·o (rankβπ§)) +o ((πΊβsuc (rankβπ§))βπ§)) β ((rankβπ¦) = (rankβπ§) β§ ((πΊβsuc (rankβπ¦))βπ¦) = ((πΊβsuc (rankβπ§))βπ§)))) |
201 | 190 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ πΆ = βͺ πΆ) β§ (rankβπ¦) = (rankβπ§)) β suc (rankβπ¦) = suc (rankβπ§)) |
202 | 201 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ ((((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ πΆ = βͺ πΆ) β§ (rankβπ¦) = (rankβπ§)) β (πΊβsuc (rankβπ¦)) = (πΊβsuc (rankβπ§))) |
203 | 202 | fveq1d 6845 |
. . . . . . . . . . 11
β’ ((((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ πΆ = βͺ πΆ) β§ (rankβπ¦) = (rankβπ§)) β ((πΊβsuc (rankβπ¦))βπ§) = ((πΊβsuc (rankβπ§))βπ§)) |
204 | 203 | eqeq2d 2748 |
. . . . . . . . . 10
β’ ((((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ πΆ = βͺ πΆ) β§ (rankβπ¦) = (rankβπ§)) β (((πΊβsuc (rankβπ¦))βπ¦) = ((πΊβsuc (rankβπ¦))βπ§) β ((πΊβsuc (rankβπ¦))βπ¦) = ((πΊβsuc (rankβπ§))βπ§))) |
205 | 64 | adantlrr 720 |
. . . . . . . . . . . 12
β’ (((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ πΆ = βͺ πΆ) β (πΊβsuc (rankβπ¦)):(π
1βsuc
(rankβπ¦))β1-1βOn) |
206 | 205 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ πΆ = βͺ πΆ) β§ (rankβπ¦) = (rankβπ§)) β (πΊβsuc (rankβπ¦)):(π
1βsuc
(rankβπ¦))β1-1βOn) |
207 | 70 | adantlrr 720 |
. . . . . . . . . . . 12
β’ (((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ πΆ = βͺ πΆ) β π¦ β (π
1βsuc
(rankβπ¦))) |
208 | 207 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ πΆ = βͺ πΆ) β§ (rankβπ¦) = (rankβπ§)) β π¦ β (π
1βsuc
(rankβπ¦))) |
209 | | r1elwf 9733 |
. . . . . . . . . . . . . . 15
β’ (π§ β
(π
1βπΆ) β π§ β βͺ
(π
1 β On)) |
210 | | rankidb 9737 |
. . . . . . . . . . . . . . 15
β’ (π§ β βͺ (π
1 β On) β π§ β
(π
1βsuc (rankβπ§))) |
211 | 209, 210 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π§ β
(π
1βπΆ) β π§ β (π
1βsuc
(rankβπ§))) |
212 | 211 | ad2antll 728 |
. . . . . . . . . . . . 13
β’ ((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β π§ β (π
1βsuc
(rankβπ§))) |
213 | 212 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ πΆ = βͺ πΆ) β§ (rankβπ¦) = (rankβπ§)) β π§ β (π
1βsuc
(rankβπ§))) |
214 | 201 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ ((((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ πΆ = βͺ πΆ) β§ (rankβπ¦) = (rankβπ§)) β
(π
1βsuc (rankβπ¦)) = (π
1βsuc
(rankβπ§))) |
215 | 213, 214 | eleqtrrd 2841 |
. . . . . . . . . . 11
β’ ((((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ πΆ = βͺ πΆ) β§ (rankβπ¦) = (rankβπ§)) β π§ β (π
1βsuc
(rankβπ¦))) |
216 | | f1fveq 7210 |
. . . . . . . . . . 11
β’ (((πΊβsuc (rankβπ¦)):(π
1βsuc
(rankβπ¦))β1-1βOn β§ (π¦ β (π
1βsuc
(rankβπ¦)) β§ π§ β
(π
1βsuc (rankβπ¦)))) β (((πΊβsuc (rankβπ¦))βπ¦) = ((πΊβsuc (rankβπ¦))βπ§) β π¦ = π§)) |
217 | 206, 208,
215, 216 | syl12anc 836 |
. . . . . . . . . 10
β’ ((((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ πΆ = βͺ πΆ) β§ (rankβπ¦) = (rankβπ§)) β (((πΊβsuc (rankβπ¦))βπ¦) = ((πΊβsuc (rankβπ¦))βπ§) β π¦ = π§)) |
218 | 204, 217 | bitr3d 281 |
. . . . . . . . 9
β’ ((((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ πΆ = βͺ πΆ) β§ (rankβπ¦) = (rankβπ§)) β (((πΊβsuc (rankβπ¦))βπ¦) = ((πΊβsuc (rankβπ§))βπ§) β π¦ = π§)) |
219 | 218 | biimpd 228 |
. . . . . . . 8
β’ ((((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ πΆ = βͺ πΆ) β§ (rankβπ¦) = (rankβπ§)) β (((πΊβsuc (rankβπ¦))βπ¦) = ((πΊβsuc (rankβπ§))βπ§) β π¦ = π§)) |
220 | 219 | expimpd 455 |
. . . . . . 7
β’ (((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ πΆ = βͺ πΆ) β (((rankβπ¦) = (rankβπ§) β§ ((πΊβsuc (rankβπ¦))βπ¦) = ((πΊβsuc (rankβπ§))βπ§)) β π¦ = π§)) |
221 | 189, 194 | jca 513 |
. . . . . . 7
β’ (π¦ = π§ β ((rankβπ¦) = (rankβπ§) β§ ((πΊβsuc (rankβπ¦))βπ¦) = ((πΊβsuc (rankβπ§))βπ§))) |
222 | 220, 221 | impbid1 224 |
. . . . . 6
β’ (((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ πΆ = βͺ πΆ) β (((rankβπ¦) = (rankβπ§) β§ ((πΊβsuc (rankβπ¦))βπ¦) = ((πΊβsuc (rankβπ§))βπ§)) β π¦ = π§)) |
223 | 163, 200,
222 | 3bitrd 305 |
. . . . 5
β’ (((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ πΆ = βͺ πΆ) β (if(πΆ = βͺ πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)), (πΉβ(π» β π¦))) = if(πΆ = βͺ πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ§)) +o ((πΊβsuc (rankβπ§))βπ§)), (πΉβ(π» β π§))) β π¦ = π§)) |
224 | | iffalse 4496 |
. . . . . . . 8
β’ (Β¬
πΆ = βͺ πΆ
β if(πΆ = βͺ πΆ,
((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)), (πΉβ(π» β π¦))) = (πΉβ(π» β π¦))) |
225 | | iffalse 4496 |
. . . . . . . 8
β’ (Β¬
πΆ = βͺ πΆ
β if(πΆ = βͺ πΆ,
((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ§)) +o ((πΊβsuc (rankβπ§))βπ§)), (πΉβ(π» β π§))) = (πΉβ(π» β π§))) |
226 | 224, 225 | eqeq12d 2753 |
. . . . . . 7
β’ (Β¬
πΆ = βͺ πΆ
β (if(πΆ = βͺ πΆ,
((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)), (πΉβ(π» β π¦))) = if(πΆ = βͺ πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ§)) +o ((πΊβsuc (rankβπ§))βπ§)), (πΉβ(π» β π§))) β (πΉβ(π» β π¦)) = (πΉβ(π» β π§)))) |
227 | 226 | adantl 483 |
. . . . . 6
β’ (((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ Β¬ πΆ = βͺ
πΆ) β (if(πΆ = βͺ
πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)), (πΉβ(π» β π¦))) = if(πΆ = βͺ πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ§)) +o ((πΊβsuc (rankβπ§))βπ§)), (πΉβ(π» β π§))) β (πΉβ(π» β π¦)) = (πΉβ(π» β π§)))) |
228 | 74 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ Β¬ πΆ = βͺ
πΆ) β πΉ:π«
(harβ(π
1βπ΄))β1-1βOn) |
229 | 156 | adantlrr 720 |
. . . . . . 7
β’ (((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ Β¬ πΆ = βͺ
πΆ) β (π» β π¦) β π«
(harβ(π
1βπ΄))) |
230 | 187 | anbi1d 631 |
. . . . . . . . . 10
β’ (π¦ = π§ β (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β ((π β§ π§ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ))) |
231 | | imaeq2 6010 |
. . . . . . . . . . 11
β’ (π¦ = π§ β (π» β π¦) = (π» β π§)) |
232 | 231 | eleq1d 2823 |
. . . . . . . . . 10
β’ (π¦ = π§ β ((π» β π¦) β π«
(harβ(π
1βπ΄)) β (π» β π§) β π«
(harβ(π
1βπ΄)))) |
233 | 230, 232 | imbi12d 345 |
. . . . . . . . 9
β’ (π¦ = π§ β ((((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β (π» β π¦) β π«
(harβ(π
1βπ΄))) β (((π β§ π§ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β (π» β π§) β π«
(harβ(π
1βπ΄))))) |
234 | 233, 156 | chvarvv 2003 |
. . . . . . . 8
β’ (((π β§ π§ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β (π» β π§) β π«
(harβ(π
1βπ΄))) |
235 | 234 | adantlrl 719 |
. . . . . . 7
β’ (((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ Β¬ πΆ = βͺ
πΆ) β (π» β π§) β π«
(harβ(π
1βπ΄))) |
236 | | f1fveq 7210 |
. . . . . . 7
β’ ((πΉ:π«
(harβ(π
1βπ΄))β1-1βOn β§ ((π» β π¦) β π«
(harβ(π
1βπ΄)) β§ (π» β π§) β π«
(harβ(π
1βπ΄)))) β ((πΉβ(π» β π¦)) = (πΉβ(π» β π§)) β (π» β π¦) = (π» β π§))) |
237 | 228, 229,
235, 236 | syl12anc 836 |
. . . . . 6
β’ (((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ Β¬ πΆ = βͺ
πΆ) β ((πΉβ(π» β π¦)) = (πΉβ(π» β π§)) β (π» β π¦) = (π» β π§))) |
238 | 120 | adantlrr 720 |
. . . . . . 7
β’ (((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ Β¬ πΆ = βͺ
πΆ) β π»:(π
1ββͺ πΆ)β1-1βdom OrdIso( E , ran (πΊββͺ πΆ))) |
239 | | simplrl 776 |
. . . . . . . . 9
β’ (((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ Β¬ πΆ = βͺ
πΆ) β π¦ β
(π
1βπΆ)) |
240 | 96 | fveq2d 6847 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β
(π
1βπΆ) = (π
1βsuc βͺ πΆ)) |
241 | | r1suc 9707 |
. . . . . . . . . . . 12
β’ (βͺ πΆ
β On β (π
1βsuc βͺ
πΆ) = π«
(π
1ββͺ πΆ)) |
242 | 89, 90, 241 | 3syl 18 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β
(π
1βsuc βͺ πΆ) = π«
(π
1ββͺ πΆ)) |
243 | 240, 242 | eqtrd 2777 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β
(π
1βπΆ) = π«
(π
1ββͺ πΆ)) |
244 | 243 | adantlrr 720 |
. . . . . . . . 9
β’ (((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ Β¬ πΆ = βͺ
πΆ) β
(π
1βπΆ) = π«
(π
1ββͺ πΆ)) |
245 | 239, 244 | eleqtrd 2840 |
. . . . . . . 8
β’ (((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ Β¬ πΆ = βͺ
πΆ) β π¦ β π«
(π
1ββͺ πΆ)) |
246 | 245 | elpwid 4570 |
. . . . . . 7
β’ (((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ Β¬ πΆ = βͺ
πΆ) β π¦ β
(π
1ββͺ πΆ)) |
247 | | simplrr 777 |
. . . . . . . . 9
β’ (((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ Β¬ πΆ = βͺ
πΆ) β π§ β
(π
1βπΆ)) |
248 | 247, 244 | eleqtrd 2840 |
. . . . . . . 8
β’ (((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ Β¬ πΆ = βͺ
πΆ) β π§ β π«
(π
1ββͺ πΆ)) |
249 | 248 | elpwid 4570 |
. . . . . . 7
β’ (((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ Β¬ πΆ = βͺ
πΆ) β π§ β
(π
1ββͺ πΆ)) |
250 | | f1imaeq 7213 |
. . . . . . 7
β’ ((π»:(π
1ββͺ πΆ)β1-1βdom OrdIso( E , ran (πΊββͺ πΆ)) β§ (π¦ β (π
1ββͺ πΆ)
β§ π§ β
(π
1ββͺ πΆ))) β ((π» β π¦) = (π» β π§) β π¦ = π§)) |
251 | 238, 246,
249, 250 | syl12anc 836 |
. . . . . 6
β’ (((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ Β¬ πΆ = βͺ
πΆ) β ((π» β π¦) = (π» β π§) β π¦ = π§)) |
252 | 227, 237,
251 | 3bitrd 305 |
. . . . 5
β’ (((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β§ Β¬ πΆ = βͺ
πΆ) β (if(πΆ = βͺ
πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)), (πΉβ(π» β π¦))) = if(πΆ = βͺ πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ§)) +o ((πΊβsuc (rankβπ§))βπ§)), (πΉβ(π» β π§))) β π¦ = π§)) |
253 | 223, 252 | pm2.61dan 812 |
. . . 4
β’ ((π β§ (π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ))) β (if(πΆ = βͺ πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)), (πΉβ(π» β π¦))) = if(πΆ = βͺ πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ§)) +o ((πΊβsuc (rankβπ§))βπ§)), (πΉβ(π» β π§))) β π¦ = π§)) |
254 | 253 | ex 414 |
. . 3
β’ (π β ((π¦ β (π
1βπΆ) β§ π§ β (π
1βπΆ)) β (if(πΆ = βͺ πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)), (πΉβ(π» β π¦))) = if(πΆ = βͺ πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ§)) +o ((πΊβsuc (rankβπ§))βπ§)), (πΉβ(π» β π§))) β π¦ = π§))) |
255 | 159, 254 | dom2lem 8933 |
. 2
β’ (π β (π¦ β (π
1βπΆ) β¦ if(πΆ = βͺ πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)), (πΉβ(π» β π¦)))):(π
1βπΆ)β1-1βOn) |
256 | 135, 74, 1, 5, 117 | dfac12lem1 10080 |
. . 3
β’ (π β (πΊβπΆ) = (π¦ β (π
1βπΆ) β¦ if(πΆ = βͺ πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)), (πΉβ(π» β π¦))))) |
257 | | f1eq1 6734 |
. . 3
β’ ((πΊβπΆ) = (π¦ β (π
1βπΆ) β¦ if(πΆ = βͺ πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)), (πΉβ(π» β π¦)))) β ((πΊβπΆ):(π
1βπΆ)β1-1βOn β (π¦ β (π
1βπΆ) β¦ if(πΆ = βͺ πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)), (πΉβ(π» β π¦)))):(π
1βπΆ)β1-1βOn)) |
258 | 256, 257 | syl 17 |
. 2
β’ (π β ((πΊβπΆ):(π
1βπΆ)β1-1βOn β (π¦ β (π
1βπΆ) β¦ if(πΆ = βͺ πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)), (πΉβ(π» β π¦)))):(π
1βπΆ)β1-1βOn)) |
259 | 255, 258 | mpbird 257 |
1
β’ (π β (πΊβπΆ):(π
1βπΆ)β1-1βOn) |