Step | Hyp | Ref
| Expression |
1 | | dfac12.5 |
. . 3
β’ (π β πΆ β On) |
2 | | dfac12.4 |
. . . 4
β’ πΊ = recs((π₯ β V β¦ (π¦ β (π
1βdom
π₯) β¦ if(dom π₯ = βͺ
dom π₯, ((suc βͺ ran βͺ ran π₯ Β·o (rankβπ¦)) +o ((π₯βsuc (rankβπ¦))βπ¦)), (πΉβ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π¦)))))) |
3 | 2 | tfr2 8345 |
. . 3
β’ (πΆ β On β (πΊβπΆ) = ((π₯ β V β¦ (π¦ β (π
1βdom
π₯) β¦ if(dom π₯ = βͺ
dom π₯, ((suc βͺ ran βͺ ran π₯ Β·o (rankβπ¦)) +o ((π₯βsuc (rankβπ¦))βπ¦)), (πΉβ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π¦)))))β(πΊ βΎ πΆ))) |
4 | 1, 3 | syl 17 |
. 2
β’ (π β (πΊβπΆ) = ((π₯ β V β¦ (π¦ β (π
1βdom
π₯) β¦ if(dom π₯ = βͺ
dom π₯, ((suc βͺ ran βͺ ran π₯ Β·o (rankβπ¦)) +o ((π₯βsuc (rankβπ¦))βπ¦)), (πΉβ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π¦)))))β(πΊ βΎ πΆ))) |
5 | 2 | tfr1 8344 |
. . . . 5
β’ πΊ Fn On |
6 | | fnfun 6603 |
. . . . 5
β’ (πΊ Fn On β Fun πΊ) |
7 | 5, 6 | ax-mp 5 |
. . . 4
β’ Fun πΊ |
8 | | resfunexg 7166 |
. . . 4
β’ ((Fun
πΊ β§ πΆ β On) β (πΊ βΎ πΆ) β V) |
9 | 7, 1, 8 | sylancr 588 |
. . 3
β’ (π β (πΊ βΎ πΆ) β V) |
10 | | dmeq 5860 |
. . . . . 6
β’ (π₯ = (πΊ βΎ πΆ) β dom π₯ = dom (πΊ βΎ πΆ)) |
11 | 10 | fveq2d 6847 |
. . . . 5
β’ (π₯ = (πΊ βΎ πΆ) β (π
1βdom
π₯) =
(π
1βdom (πΊ βΎ πΆ))) |
12 | 10 | unieqd 4880 |
. . . . . . 7
β’ (π₯ = (πΊ βΎ πΆ) β βͺ dom
π₯ = βͺ dom (πΊ βΎ πΆ)) |
13 | 10, 12 | eqeq12d 2753 |
. . . . . 6
β’ (π₯ = (πΊ βΎ πΆ) β (dom π₯ = βͺ dom π₯ β dom (πΊ βΎ πΆ) = βͺ dom (πΊ βΎ πΆ))) |
14 | | rneq 5892 |
. . . . . . . . . . . . 13
β’ (π₯ = (πΊ βΎ πΆ) β ran π₯ = ran (πΊ βΎ πΆ)) |
15 | | df-ima 5647 |
. . . . . . . . . . . . 13
β’ (πΊ β πΆ) = ran (πΊ βΎ πΆ) |
16 | 14, 15 | eqtr4di 2795 |
. . . . . . . . . . . 12
β’ (π₯ = (πΊ βΎ πΆ) β ran π₯ = (πΊ β πΆ)) |
17 | 16 | unieqd 4880 |
. . . . . . . . . . 11
β’ (π₯ = (πΊ βΎ πΆ) β βͺ ran
π₯ = βͺ (πΊ
β πΆ)) |
18 | 17 | rneqd 5894 |
. . . . . . . . . 10
β’ (π₯ = (πΊ βΎ πΆ) β ran βͺ
ran π₯ = ran βͺ (πΊ
β πΆ)) |
19 | 18 | unieqd 4880 |
. . . . . . . . 9
β’ (π₯ = (πΊ βΎ πΆ) β βͺ ran
βͺ ran π₯ = βͺ ran βͺ (πΊ
β πΆ)) |
20 | | suceq 6384 |
. . . . . . . . 9
β’ (βͺ ran βͺ ran π₯ = βͺ ran βͺ (πΊ
β πΆ) β suc βͺ ran βͺ ran π₯ = suc βͺ ran βͺ (πΊ
β πΆ)) |
21 | 19, 20 | syl 17 |
. . . . . . . 8
β’ (π₯ = (πΊ βΎ πΆ) β suc βͺ
ran βͺ ran π₯ = suc βͺ ran βͺ (πΊ
β πΆ)) |
22 | 21 | oveq1d 7373 |
. . . . . . 7
β’ (π₯ = (πΊ βΎ πΆ) β (suc βͺ
ran βͺ ran π₯ Β·o (rankβπ¦)) = (suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦))) |
23 | | fveq1 6842 |
. . . . . . . 8
β’ (π₯ = (πΊ βΎ πΆ) β (π₯βsuc (rankβπ¦)) = ((πΊ βΎ πΆ)βsuc (rankβπ¦))) |
24 | 23 | fveq1d 6845 |
. . . . . . 7
β’ (π₯ = (πΊ βΎ πΆ) β ((π₯βsuc (rankβπ¦))βπ¦) = (((πΊ βΎ πΆ)βsuc (rankβπ¦))βπ¦)) |
25 | 22, 24 | oveq12d 7376 |
. . . . . 6
β’ (π₯ = (πΊ βΎ πΆ) β ((suc βͺ
ran βͺ ran π₯ Β·o (rankβπ¦)) +o ((π₯βsuc (rankβπ¦))βπ¦)) = ((suc βͺ ran
βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o (((πΊ βΎ πΆ)βsuc (rankβπ¦))βπ¦))) |
26 | | id 22 |
. . . . . . . . . . . . 13
β’ (π₯ = (πΊ βΎ πΆ) β π₯ = (πΊ βΎ πΆ)) |
27 | 26, 12 | fveq12d 6850 |
. . . . . . . . . . . 12
β’ (π₯ = (πΊ βΎ πΆ) β (π₯ββͺ dom π₯) = ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) |
28 | 27 | rneqd 5894 |
. . . . . . . . . . 11
β’ (π₯ = (πΊ βΎ πΆ) β ran (π₯ββͺ dom π₯) = ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) |
29 | | oieq2 9450 |
. . . . . . . . . . 11
β’ (ran
(π₯ββͺ dom π₯) = ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ)) β OrdIso( E , ran (π₯ββͺ dom π₯)) = OrdIso( E , ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ)))) |
30 | 28, 29 | syl 17 |
. . . . . . . . . 10
β’ (π₯ = (πΊ βΎ πΆ) β OrdIso( E , ran (π₯ββͺ dom π₯)) = OrdIso( E , ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ)))) |
31 | 30 | cnveqd 5832 |
. . . . . . . . 9
β’ (π₯ = (πΊ βΎ πΆ) β β‘OrdIso( E , ran (π₯ββͺ dom π₯)) = β‘OrdIso( E , ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ)))) |
32 | 31, 27 | coeq12d 5821 |
. . . . . . . 8
β’ (π₯ = (πΊ βΎ πΆ) β (β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) = (β‘OrdIso( E , ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ)))) |
33 | 32 | imaeq1d 6013 |
. . . . . . 7
β’ (π₯ = (πΊ βΎ πΆ) β ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π¦) = ((β‘OrdIso( E , ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β π¦)) |
34 | 33 | fveq2d 6847 |
. . . . . 6
β’ (π₯ = (πΊ βΎ πΆ) β (πΉβ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π¦)) = (πΉβ((β‘OrdIso( E , ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β π¦))) |
35 | 13, 25, 34 | ifbieq12d 4515 |
. . . . 5
β’ (π₯ = (πΊ βΎ πΆ) β if(dom π₯ = βͺ dom π₯, ((suc βͺ ran βͺ ran π₯ Β·o (rankβπ¦)) +o ((π₯βsuc (rankβπ¦))βπ¦)), (πΉβ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π¦))) = if(dom (πΊ βΎ πΆ) = βͺ dom (πΊ βΎ πΆ), ((suc βͺ ran
βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o (((πΊ βΎ πΆ)βsuc (rankβπ¦))βπ¦)), (πΉβ((β‘OrdIso( E , ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β π¦)))) |
36 | 11, 35 | mpteq12dv 5197 |
. . . 4
β’ (π₯ = (πΊ βΎ πΆ) β (π¦ β (π
1βdom
π₯) β¦ if(dom π₯ = βͺ
dom π₯, ((suc βͺ ran βͺ ran π₯ Β·o (rankβπ¦)) +o ((π₯βsuc (rankβπ¦))βπ¦)), (πΉβ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π¦)))) = (π¦ β (π
1βdom
(πΊ βΎ πΆ)) β¦ if(dom (πΊ βΎ πΆ) = βͺ dom (πΊ βΎ πΆ), ((suc βͺ ran
βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o (((πΊ βΎ πΆ)βsuc (rankβπ¦))βπ¦)), (πΉβ((β‘OrdIso( E , ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β π¦))))) |
37 | | eqid 2737 |
. . . 4
β’ (π₯ β V β¦ (π¦ β
(π
1βdom π₯) β¦ if(dom π₯ = βͺ dom π₯, ((suc βͺ ran βͺ ran π₯ Β·o (rankβπ¦)) +o ((π₯βsuc (rankβπ¦))βπ¦)), (πΉβ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π¦))))) = (π₯ β V β¦ (π¦ β (π
1βdom
π₯) β¦ if(dom π₯ = βͺ
dom π₯, ((suc βͺ ran βͺ ran π₯ Β·o (rankβπ¦)) +o ((π₯βsuc (rankβπ¦))βπ¦)), (πΉβ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π¦))))) |
38 | | fvex 6856 |
. . . . 5
β’
(π
1βdom (πΊ βΎ πΆ)) β V |
39 | 38 | mptex 7174 |
. . . 4
β’ (π¦ β
(π
1βdom (πΊ βΎ πΆ)) β¦ if(dom (πΊ βΎ πΆ) = βͺ dom (πΊ βΎ πΆ), ((suc βͺ ran
βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o (((πΊ βΎ πΆ)βsuc (rankβπ¦))βπ¦)), (πΉβ((β‘OrdIso( E , ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β π¦)))) β V |
40 | 36, 37, 39 | fvmpt 6949 |
. . 3
β’ ((πΊ βΎ πΆ) β V β ((π₯ β V β¦ (π¦ β (π
1βdom
π₯) β¦ if(dom π₯ = βͺ
dom π₯, ((suc βͺ ran βͺ ran π₯ Β·o (rankβπ¦)) +o ((π₯βsuc (rankβπ¦))βπ¦)), (πΉβ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π¦)))))β(πΊ βΎ πΆ)) = (π¦ β (π
1βdom
(πΊ βΎ πΆ)) β¦ if(dom (πΊ βΎ πΆ) = βͺ dom (πΊ βΎ πΆ), ((suc βͺ ran
βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o (((πΊ βΎ πΆ)βsuc (rankβπ¦))βπ¦)), (πΉβ((β‘OrdIso( E , ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β π¦))))) |
41 | 9, 40 | syl 17 |
. 2
β’ (π β ((π₯ β V β¦ (π¦ β (π
1βdom
π₯) β¦ if(dom π₯ = βͺ
dom π₯, ((suc βͺ ran βͺ ran π₯ Β·o (rankβπ¦)) +o ((π₯βsuc (rankβπ¦))βπ¦)), (πΉβ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π¦)))))β(πΊ βΎ πΆ)) = (π¦ β (π
1βdom
(πΊ βΎ πΆ)) β¦ if(dom (πΊ βΎ πΆ) = βͺ dom (πΊ βΎ πΆ), ((suc βͺ ran
βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o (((πΊ βΎ πΆ)βsuc (rankβπ¦))βπ¦)), (πΉβ((β‘OrdIso( E , ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β π¦))))) |
42 | | onss 7720 |
. . . . . . . 8
β’ (πΆ β On β πΆ β On) |
43 | 1, 42 | syl 17 |
. . . . . . 7
β’ (π β πΆ β On) |
44 | | fnssres 6625 |
. . . . . . 7
β’ ((πΊ Fn On β§ πΆ β On) β (πΊ βΎ πΆ) Fn πΆ) |
45 | 5, 43, 44 | sylancr 588 |
. . . . . 6
β’ (π β (πΊ βΎ πΆ) Fn πΆ) |
46 | 45 | fndmd 6608 |
. . . . 5
β’ (π β dom (πΊ βΎ πΆ) = πΆ) |
47 | 46 | fveq2d 6847 |
. . . 4
β’ (π β
(π
1βdom (πΊ βΎ πΆ)) = (π
1βπΆ)) |
48 | 47 | mpteq1d 5201 |
. . 3
β’ (π β (π¦ β (π
1βdom
(πΊ βΎ πΆ)) β¦ if(dom (πΊ βΎ πΆ) = βͺ dom (πΊ βΎ πΆ), ((suc βͺ ran
βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o (((πΊ βΎ πΆ)βsuc (rankβπ¦))βπ¦)), (πΉβ((β‘OrdIso( E , ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β π¦)))) = (π¦ β (π
1βπΆ) β¦ if(dom (πΊ βΎ πΆ) = βͺ dom (πΊ βΎ πΆ), ((suc βͺ ran
βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o (((πΊ βΎ πΆ)βsuc (rankβπ¦))βπ¦)), (πΉβ((β‘OrdIso( E , ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β π¦))))) |
49 | 46 | adantr 482 |
. . . . . . 7
β’ ((π β§ π¦ β (π
1βπΆ)) β dom (πΊ βΎ πΆ) = πΆ) |
50 | 49 | unieqd 4880 |
. . . . . . 7
β’ ((π β§ π¦ β (π
1βπΆ)) β βͺ dom (πΊ βΎ πΆ) = βͺ πΆ) |
51 | 49, 50 | eqeq12d 2753 |
. . . . . 6
β’ ((π β§ π¦ β (π
1βπΆ)) β (dom (πΊ βΎ πΆ) = βͺ dom (πΊ βΎ πΆ) β πΆ = βͺ πΆ)) |
52 | 51 | ifbid 4510 |
. . . . 5
β’ ((π β§ π¦ β (π
1βπΆ)) β if(dom (πΊ βΎ πΆ) = βͺ dom (πΊ βΎ πΆ), ((suc βͺ ran
βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o (((πΊ βΎ πΆ)βsuc (rankβπ¦))βπ¦)), (πΉβ((β‘OrdIso( E , ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β π¦))) = if(πΆ = βͺ πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o (((πΊ βΎ πΆ)βsuc (rankβπ¦))βπ¦)), (πΉβ((β‘OrdIso( E , ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β π¦)))) |
53 | | rankr1ai 9735 |
. . . . . . . . . . . 12
β’ (π¦ β
(π
1βπΆ) β (rankβπ¦) β πΆ) |
54 | 53 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β (rankβπ¦) β πΆ) |
55 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β πΆ = βͺ πΆ) |
56 | 54, 55 | eleqtrd 2840 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β (rankβπ¦) β βͺ πΆ) |
57 | | eloni 6328 |
. . . . . . . . . . . 12
β’ (πΆ β On β Ord πΆ) |
58 | | ordsucuniel 7760 |
. . . . . . . . . . . 12
β’ (Ord
πΆ β ((rankβπ¦) β βͺ πΆ
β suc (rankβπ¦)
β πΆ)) |
59 | 1, 57, 58 | 3syl 18 |
. . . . . . . . . . 11
β’ (π β ((rankβπ¦) β βͺ πΆ
β suc (rankβπ¦)
β πΆ)) |
60 | 59 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β ((rankβπ¦) β βͺ πΆ
β suc (rankβπ¦)
β πΆ)) |
61 | 56, 60 | mpbid 231 |
. . . . . . . . 9
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β suc (rankβπ¦) β πΆ) |
62 | 61 | fvresd 6863 |
. . . . . . . 8
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β ((πΊ βΎ πΆ)βsuc (rankβπ¦)) = (πΊβsuc (rankβπ¦))) |
63 | 62 | fveq1d 6845 |
. . . . . . 7
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β (((πΊ βΎ πΆ)βsuc (rankβπ¦))βπ¦) = ((πΊβsuc (rankβπ¦))βπ¦)) |
64 | 63 | oveq2d 7374 |
. . . . . 6
β’ (((π β§ π¦ β (π
1βπΆ)) β§ πΆ = βͺ πΆ) β ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o (((πΊ βΎ πΆ)βsuc (rankβπ¦))βπ¦)) = ((suc βͺ ran
βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦))) |
65 | 64 | ifeq1da 4518 |
. . . . 5
β’ ((π β§ π¦ β (π
1βπΆ)) β if(πΆ = βͺ πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o (((πΊ βΎ πΆ)βsuc (rankβπ¦))βπ¦)), (πΉβ((β‘OrdIso( E , ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β π¦))) = if(πΆ = βͺ πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)), (πΉβ((β‘OrdIso( E , ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β π¦)))) |
66 | 50 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β βͺ dom (πΊ βΎ πΆ) = βͺ πΆ) |
67 | 66 | fveq2d 6847 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ)) = ((πΊ βΎ πΆ)ββͺ πΆ)) |
68 | 1 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β πΆ β On) |
69 | | uniexg 7678 |
. . . . . . . . . . . . . . . . 17
β’ (πΆ β On β βͺ πΆ
β V) |
70 | | sucidg 6399 |
. . . . . . . . . . . . . . . . 17
β’ (βͺ πΆ
β V β βͺ πΆ β suc βͺ
πΆ) |
71 | 68, 69, 70 | 3syl 18 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β βͺ πΆ
β suc βͺ πΆ) |
72 | 1 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π¦ β (π
1βπΆ)) β πΆ β On) |
73 | | orduniorsuc 7766 |
. . . . . . . . . . . . . . . . . 18
β’ (Ord
πΆ β (πΆ = βͺ πΆ β¨ πΆ = suc βͺ πΆ)) |
74 | 72, 57, 73 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π¦ β (π
1βπΆ)) β (πΆ = βͺ πΆ β¨ πΆ = suc βͺ πΆ)) |
75 | 74 | orcanai 1002 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β πΆ = suc βͺ πΆ) |
76 | 71, 75 | eleqtrrd 2841 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β βͺ πΆ
β πΆ) |
77 | 76 | fvresd 6863 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β ((πΊ βΎ πΆ)ββͺ πΆ) = (πΊββͺ πΆ)) |
78 | 67, 77 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ)) = (πΊββͺ πΆ)) |
79 | 78 | rneqd 5894 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ)) = ran (πΊββͺ πΆ)) |
80 | | oieq2 9450 |
. . . . . . . . . . . 12
β’ (ran
((πΊ βΎ πΆ)ββͺ dom (πΊ βΎ πΆ)) = ran (πΊββͺ πΆ) β OrdIso( E , ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) = OrdIso( E , ran (πΊββͺ πΆ))) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β OrdIso( E , ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) = OrdIso( E , ran (πΊββͺ πΆ))) |
82 | 81 | cnveqd 5832 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β β‘OrdIso( E , ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) = β‘OrdIso( E , ran (πΊββͺ πΆ))) |
83 | 82, 78 | coeq12d 5821 |
. . . . . . . . 9
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β (β‘OrdIso( E , ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) = (β‘OrdIso( E , ran (πΊββͺ πΆ)) β (πΊββͺ πΆ))) |
84 | | dfac12.h |
. . . . . . . . 9
β’ π» = (β‘OrdIso( E , ran (πΊββͺ πΆ)) β (πΊββͺ πΆ)) |
85 | 83, 84 | eqtr4di 2795 |
. . . . . . . 8
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β (β‘OrdIso( E , ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) = π») |
86 | 85 | imaeq1d 6013 |
. . . . . . 7
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β ((β‘OrdIso( E , ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β π¦) = (π» β π¦)) |
87 | 86 | fveq2d 6847 |
. . . . . 6
β’ (((π β§ π¦ β (π
1βπΆ)) β§ Β¬ πΆ = βͺ πΆ) β (πΉβ((β‘OrdIso( E , ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β π¦)) = (πΉβ(π» β π¦))) |
88 | 87 | ifeq2da 4519 |
. . . . 5
β’ ((π β§ π¦ β (π
1βπΆ)) β if(πΆ = βͺ πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)), (πΉβ((β‘OrdIso( E , ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β π¦))) = if(πΆ = βͺ πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)), (πΉβ(π» β π¦)))) |
89 | 52, 65, 88 | 3eqtrd 2781 |
. . . 4
β’ ((π β§ π¦ β (π
1βπΆ)) β if(dom (πΊ βΎ πΆ) = βͺ dom (πΊ βΎ πΆ), ((suc βͺ ran
βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o (((πΊ βΎ πΆ)βsuc (rankβπ¦))βπ¦)), (πΉβ((β‘OrdIso( E , ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β π¦))) = if(πΆ = βͺ πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)), (πΉβ(π» β π¦)))) |
90 | 89 | mpteq2dva 5206 |
. . 3
β’ (π β (π¦ β (π
1βπΆ) β¦ if(dom (πΊ βΎ πΆ) = βͺ dom (πΊ βΎ πΆ), ((suc βͺ ran
βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o (((πΊ βΎ πΆ)βsuc (rankβπ¦))βπ¦)), (πΉβ((β‘OrdIso( E , ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β π¦)))) = (π¦ β (π
1βπΆ) β¦ if(πΆ = βͺ πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)), (πΉβ(π» β π¦))))) |
91 | 48, 90 | eqtrd 2777 |
. 2
β’ (π β (π¦ β (π
1βdom
(πΊ βΎ πΆ)) β¦ if(dom (πΊ βΎ πΆ) = βͺ dom (πΊ βΎ πΆ), ((suc βͺ ran
βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o (((πΊ βΎ πΆ)βsuc (rankβπ¦))βπ¦)), (πΉβ((β‘OrdIso( E , ran ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β ((πΊ βΎ πΆ)ββͺ dom
(πΊ βΎ πΆ))) β π¦)))) = (π¦ β (π
1βπΆ) β¦ if(πΆ = βͺ πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)), (πΉβ(π» β π¦))))) |
92 | 4, 41, 91 | 3eqtrd 2781 |
1
β’ (π β (πΊβπΆ) = (π¦ β (π
1βπΆ) β¦ if(πΆ = βͺ πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)), (πΉβ(π» β π¦))))) |