Step | Hyp | Ref
| Expression |
1 | | pi1xfr.g |
. . . 4
β’ πΊ = ran (π β βͺ π΅ β¦ β¨[π](
βphβπ½), [(πΌ(*πβπ½)(π(*πβπ½)πΉ))]( βphβπ½)β©) |
2 | | fvex 6859 |
. . . . 5
β’ (
βphβπ½) β V |
3 | | ecexg 8658 |
. . . . 5
β’ ((
βphβπ½) β V β [π]( βphβπ½) β V) |
4 | 2, 3 | mp1i 13 |
. . . 4
β’ ((π β§ π β βͺ π΅) β [π]( βphβπ½) β V) |
5 | | ecexg 8658 |
. . . . 5
β’ ((
βphβπ½) β V β [(πΌ(*πβπ½)(π(*πβπ½)πΉ))]( βphβπ½) β V) |
6 | 2, 5 | mp1i 13 |
. . . 4
β’ ((π β§ π β βͺ π΅) β [(πΌ(*πβπ½)(π(*πβπ½)πΉ))]( βphβπ½) β V) |
7 | 1, 4, 6 | fliftcnv 7260 |
. . 3
β’ (π β β‘πΊ = ran (π β βͺ π΅ β¦ β¨[(πΌ(*πβπ½)(π(*πβπ½)πΉ))]( βphβπ½), [π]( βphβπ½)β©)) |
8 | | pi1xfr.f |
. . . . . . . . . . 11
β’ (π β πΉ β (II Cn π½)) |
9 | | pi1xfr.i |
. . . . . . . . . . . 12
β’ πΌ = (π₯ β (0[,]1) β¦ (πΉβ(1 β π₯))) |
10 | 9 | pcorevcl 24411 |
. . . . . . . . . . 11
β’ (πΉ β (II Cn π½) β (πΌ β (II Cn π½) β§ (πΌβ0) = (πΉβ1) β§ (πΌβ1) = (πΉβ0))) |
11 | 8, 10 | syl 17 |
. . . . . . . . . 10
β’ (π β (πΌ β (II Cn π½) β§ (πΌβ0) = (πΉβ1) β§ (πΌβ1) = (πΉβ0))) |
12 | 11 | simp1d 1143 |
. . . . . . . . 9
β’ (π β πΌ β (II Cn π½)) |
13 | 12 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β βͺ π΅) β πΌ β (II Cn π½)) |
14 | | pi1xfr.p |
. . . . . . . . . . . 12
β’ π = (π½ Ο1 (πΉβ0)) |
15 | | pi1xfr.j |
. . . . . . . . . . . 12
β’ (π β π½ β (TopOnβπ)) |
16 | | iitopon 24265 |
. . . . . . . . . . . . . 14
β’ II β
(TopOnβ(0[,]1)) |
17 | | cnf2 22623 |
. . . . . . . . . . . . . 14
β’ ((II
β (TopOnβ(0[,]1)) β§ π½ β (TopOnβπ) β§ πΉ β (II Cn π½)) β πΉ:(0[,]1)βΆπ) |
18 | 16, 15, 8, 17 | mp3an2i 1467 |
. . . . . . . . . . . . 13
β’ (π β πΉ:(0[,]1)βΆπ) |
19 | | 0elunit 13395 |
. . . . . . . . . . . . 13
β’ 0 β
(0[,]1) |
20 | | ffvelcdm 7036 |
. . . . . . . . . . . . 13
β’ ((πΉ:(0[,]1)βΆπ β§ 0 β (0[,]1)) β
(πΉβ0) β π) |
21 | 18, 19, 20 | sylancl 587 |
. . . . . . . . . . . 12
β’ (π β (πΉβ0) β π) |
22 | | pi1xfr.b |
. . . . . . . . . . . . 13
β’ π΅ = (Baseβπ) |
23 | 22 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β π΅ = (Baseβπ)) |
24 | 14, 15, 21, 23 | pi1eluni 24428 |
. . . . . . . . . . 11
β’ (π β (π β βͺ π΅ β (π β (II Cn π½) β§ (πβ0) = (πΉβ0) β§ (πβ1) = (πΉβ0)))) |
25 | 24 | biimpa 478 |
. . . . . . . . . 10
β’ ((π β§ π β βͺ π΅) β (π β (II Cn π½) β§ (πβ0) = (πΉβ0) β§ (πβ1) = (πΉβ0))) |
26 | 25 | simp1d 1143 |
. . . . . . . . 9
β’ ((π β§ π β βͺ π΅) β π β (II Cn π½)) |
27 | 8 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β βͺ π΅) β πΉ β (II Cn π½)) |
28 | 25 | simp3d 1145 |
. . . . . . . . 9
β’ ((π β§ π β βͺ π΅) β (πβ1) = (πΉβ0)) |
29 | 26, 27, 28 | pcocn 24403 |
. . . . . . . 8
β’ ((π β§ π β βͺ π΅) β (π(*πβπ½)πΉ) β (II Cn π½)) |
30 | 11 | simp3d 1145 |
. . . . . . . . . . 11
β’ (π β (πΌβ1) = (πΉβ0)) |
31 | 30 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β βͺ π΅) β (πΌβ1) = (πΉβ0)) |
32 | 25 | simp2d 1144 |
. . . . . . . . . 10
β’ ((π β§ π β βͺ π΅) β (πβ0) = (πΉβ0)) |
33 | 31, 32 | eqtr4d 2776 |
. . . . . . . . 9
β’ ((π β§ π β βͺ π΅) β (πΌβ1) = (πβ0)) |
34 | 26, 27 | pco0 24400 |
. . . . . . . . 9
β’ ((π β§ π β βͺ π΅) β ((π(*πβπ½)πΉ)β0) = (πβ0)) |
35 | 33, 34 | eqtr4d 2776 |
. . . . . . . 8
β’ ((π β§ π β βͺ π΅) β (πΌβ1) = ((π(*πβπ½)πΉ)β0)) |
36 | 13, 29, 35 | pcocn 24403 |
. . . . . . 7
β’ ((π β§ π β βͺ π΅) β (πΌ(*πβπ½)(π(*πβπ½)πΉ)) β (II Cn π½)) |
37 | 13, 29 | pco0 24400 |
. . . . . . . 8
β’ ((π β§ π β βͺ π΅) β ((πΌ(*πβπ½)(π(*πβπ½)πΉ))β0) = (πΌβ0)) |
38 | 11 | simp2d 1144 |
. . . . . . . . 9
β’ (π β (πΌβ0) = (πΉβ1)) |
39 | 38 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β βͺ π΅) β (πΌβ0) = (πΉβ1)) |
40 | 37, 39 | eqtrd 2773 |
. . . . . . 7
β’ ((π β§ π β βͺ π΅) β ((πΌ(*πβπ½)(π(*πβπ½)πΉ))β0) = (πΉβ1)) |
41 | 13, 29 | pco1 24401 |
. . . . . . . 8
β’ ((π β§ π β βͺ π΅) β ((πΌ(*πβπ½)(π(*πβπ½)πΉ))β1) = ((π(*πβπ½)πΉ)β1)) |
42 | 26, 27 | pco1 24401 |
. . . . . . . 8
β’ ((π β§ π β βͺ π΅) β ((π(*πβπ½)πΉ)β1) = (πΉβ1)) |
43 | 41, 42 | eqtrd 2773 |
. . . . . . 7
β’ ((π β§ π β βͺ π΅) β ((πΌ(*πβπ½)(π(*πβπ½)πΉ))β1) = (πΉβ1)) |
44 | | pi1xfr.q |
. . . . . . . . 9
β’ π = (π½ Ο1 (πΉβ1)) |
45 | | 1elunit 13396 |
. . . . . . . . . 10
β’ 1 β
(0[,]1) |
46 | | ffvelcdm 7036 |
. . . . . . . . . 10
β’ ((πΉ:(0[,]1)βΆπ β§ 1 β (0[,]1)) β
(πΉβ1) β π) |
47 | 18, 45, 46 | sylancl 587 |
. . . . . . . . 9
β’ (π β (πΉβ1) β π) |
48 | | eqidd 2734 |
. . . . . . . . 9
β’ (π β (Baseβπ) = (Baseβπ)) |
49 | 44, 15, 47, 48 | pi1eluni 24428 |
. . . . . . . 8
β’ (π β ((πΌ(*πβπ½)(π(*πβπ½)πΉ)) β βͺ
(Baseβπ) β
((πΌ(*πβπ½)(π(*πβπ½)πΉ)) β (II Cn π½) β§ ((πΌ(*πβπ½)(π(*πβπ½)πΉ))β0) = (πΉβ1) β§ ((πΌ(*πβπ½)(π(*πβπ½)πΉ))β1) = (πΉβ1)))) |
50 | 49 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β βͺ π΅) β ((πΌ(*πβπ½)(π(*πβπ½)πΉ)) β βͺ
(Baseβπ) β
((πΌ(*πβπ½)(π(*πβπ½)πΉ)) β (II Cn π½) β§ ((πΌ(*πβπ½)(π(*πβπ½)πΉ))β0) = (πΉβ1) β§ ((πΌ(*πβπ½)(π(*πβπ½)πΉ))β1) = (πΉβ1)))) |
51 | 36, 40, 43, 50 | mpbir3and 1343 |
. . . . . 6
β’ ((π β§ π β βͺ π΅) β (πΌ(*πβπ½)(π(*πβπ½)πΉ)) β βͺ
(Baseβπ)) |
52 | | eqidd 2734 |
. . . . . 6
β’ (π β (π β βͺ π΅ β¦ (πΌ(*πβπ½)(π(*πβπ½)πΉ))) = (π β βͺ π΅ β¦ (πΌ(*πβπ½)(π(*πβπ½)πΉ)))) |
53 | | eqidd 2734 |
. . . . . 6
β’ (π β (β β βͺ
(Baseβπ) β¦
β¨[β](
βphβπ½), [(πΉ(*πβπ½)(β(*πβπ½)πΌ))]( βphβπ½)β©) = (β β βͺ
(Baseβπ) β¦
β¨[β](
βphβπ½), [(πΉ(*πβπ½)(β(*πβπ½)πΌ))]( βphβπ½)β©)) |
54 | | eceq1 8692 |
. . . . . . 7
β’ (β = (πΌ(*πβπ½)(π(*πβπ½)πΉ)) β [β]( βphβπ½) = [(πΌ(*πβπ½)(π(*πβπ½)πΉ))]( βphβπ½)) |
55 | | oveq1 7368 |
. . . . . . . . 9
β’ (β = (πΌ(*πβπ½)(π(*πβπ½)πΉ)) β (β(*πβπ½)πΌ) = ((πΌ(*πβπ½)(π(*πβπ½)πΉ))(*πβπ½)πΌ)) |
56 | 55 | oveq2d 7377 |
. . . . . . . 8
β’ (β = (πΌ(*πβπ½)(π(*πβπ½)πΉ)) β (πΉ(*πβπ½)(β(*πβπ½)πΌ)) = (πΉ(*πβπ½)((πΌ(*πβπ½)(π(*πβπ½)πΉ))(*πβπ½)πΌ))) |
57 | 56 | eceq1d 8693 |
. . . . . . 7
β’ (β = (πΌ(*πβπ½)(π(*πβπ½)πΉ)) β [(πΉ(*πβπ½)(β(*πβπ½)πΌ))]( βphβπ½) = [(πΉ(*πβπ½)((πΌ(*πβπ½)(π(*πβπ½)πΉ))(*πβπ½)πΌ))]( βphβπ½)) |
58 | 54, 57 | opeq12d 4842 |
. . . . . 6
β’ (β = (πΌ(*πβπ½)(π(*πβπ½)πΉ)) β β¨[β]( βphβπ½), [(πΉ(*πβπ½)(β(*πβπ½)πΌ))]( βphβπ½)β© = β¨[(πΌ(*πβπ½)(π(*πβπ½)πΉ))]( βphβπ½), [(πΉ(*πβπ½)((πΌ(*πβπ½)(π(*πβπ½)πΉ))(*πβπ½)πΌ))]( βphβπ½)β©) |
59 | 51, 52, 53, 58 | fmptco 7079 |
. . . . 5
β’ (π β ((β β βͺ
(Baseβπ) β¦
β¨[β](
βphβπ½), [(πΉ(*πβπ½)(β(*πβπ½)πΌ))]( βphβπ½)β©) β (π β βͺ π΅
β¦ (πΌ(*πβπ½)(π(*πβπ½)πΉ)))) = (π β βͺ π΅ β¦ β¨[(πΌ(*πβπ½)(π(*πβπ½)πΉ))]( βphβπ½), [(πΉ(*πβπ½)((πΌ(*πβπ½)(π(*πβπ½)πΉ))(*πβπ½)πΌ))]( βphβπ½)β©)) |
60 | | phtpcer 24381 |
. . . . . . . . 9
β’ (
βphβπ½) Er (II Cn π½) |
61 | 60 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π β βͺ π΅) β (
βphβπ½) Er (II Cn π½)) |
62 | 13, 26 | pco0 24400 |
. . . . . . . . . . 11
β’ ((π β§ π β βͺ π΅) β ((πΌ(*πβπ½)π)β0) = (πΌβ0)) |
63 | 62, 39 | eqtr2d 2774 |
. . . . . . . . . 10
β’ ((π β§ π β βͺ π΅) β (πΉβ1) = ((πΌ(*πβπ½)π)β0)) |
64 | 61, 27 | erref 8674 |
. . . . . . . . . 10
β’ ((π β§ π β βͺ π΅) β πΉ( βphβπ½)πΉ) |
65 | 61, 13 | erref 8674 |
. . . . . . . . . . . 12
β’ ((π β§ π β βͺ π΅) β πΌ( βphβπ½)πΌ) |
66 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ ((0[,]1)
Γ {(πΉβ0)}) =
((0[,]1) Γ {(πΉβ0)}) |
67 | 66 | pcopt2 24409 |
. . . . . . . . . . . . . 14
β’ ((π β (II Cn π½) β§ (πβ1) = (πΉβ0)) β (π(*πβπ½)((0[,]1) Γ {(πΉβ0)}))(
βphβπ½)π) |
68 | 26, 28, 67 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π β βͺ π΅) β (π(*πβπ½)((0[,]1) Γ {(πΉβ0)}))(
βphβπ½)π) |
69 | 39 | eqcomd 2739 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β βͺ π΅) β (πΉβ1) = (πΌβ0)) |
70 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (0[,]1) β¦ if(π₯ β€ (1 / 2), if(π₯ β€ (1 / 4), (2 Β· π₯), (π₯ + (1 / 4))), ((π₯ / 2) + (1 / 2)))) = (π₯ β (0[,]1) β¦ if(π₯ β€ (1 / 2), if(π₯ β€ (1 / 4), (2 Β· π₯), (π₯ + (1 / 4))), ((π₯ / 2) + (1 / 2)))) |
71 | 26, 27, 13, 28, 69, 70 | pcoass 24410 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β βͺ π΅) β ((π(*πβπ½)πΉ)(*πβπ½)πΌ)( βphβπ½)(π(*πβπ½)(πΉ(*πβπ½)πΌ))) |
72 | 27, 13 | pco0 24400 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β βͺ π΅) β ((πΉ(*πβπ½)πΌ)β0) = (πΉβ0)) |
73 | 28, 72 | eqtr4d 2776 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β βͺ π΅) β (πβ1) = ((πΉ(*πβπ½)πΌ)β0)) |
74 | 61, 26 | erref 8674 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β βͺ π΅) β π( βphβπ½)π) |
75 | 9, 66 | pcorev2 24414 |
. . . . . . . . . . . . . . . 16
β’ (πΉ β (II Cn π½) β (πΉ(*πβπ½)πΌ)( βphβπ½)((0[,]1) Γ {(πΉβ0)})) |
76 | 27, 75 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β βͺ π΅) β (πΉ(*πβπ½)πΌ)( βphβπ½)((0[,]1) Γ {(πΉβ0)})) |
77 | 73, 74, 76 | pcohtpy 24406 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β βͺ π΅) β (π(*πβπ½)(πΉ(*πβπ½)πΌ))( βphβπ½)(π(*πβπ½)((0[,]1) Γ {(πΉβ0)}))) |
78 | 61, 71, 77 | ertr2d 8671 |
. . . . . . . . . . . . 13
β’ ((π β§ π β βͺ π΅) β (π(*πβπ½)((0[,]1) Γ {(πΉβ0)}))(
βphβπ½)((π(*πβπ½)πΉ)(*πβπ½)πΌ)) |
79 | 61, 68, 78 | ertr3d 8672 |
. . . . . . . . . . . 12
β’ ((π β§ π β βͺ π΅) β π( βphβπ½)((π(*πβπ½)πΉ)(*πβπ½)πΌ)) |
80 | 33, 65, 79 | pcohtpy 24406 |
. . . . . . . . . . 11
β’ ((π β§ π β βͺ π΅) β (πΌ(*πβπ½)π)( βphβπ½)(πΌ(*πβπ½)((π(*πβπ½)πΉ)(*πβπ½)πΌ))) |
81 | 42, 39 | eqtr4d 2776 |
. . . . . . . . . . . 12
β’ ((π β§ π β βͺ π΅) β ((π(*πβπ½)πΉ)β1) = (πΌβ0)) |
82 | 13, 29, 13, 35, 81, 70 | pcoass 24410 |
. . . . . . . . . . 11
β’ ((π β§ π β βͺ π΅) β ((πΌ(*πβπ½)(π(*πβπ½)πΉ))(*πβπ½)πΌ)( βphβπ½)(πΌ(*πβπ½)((π(*πβπ½)πΉ)(*πβπ½)πΌ))) |
83 | 61, 80, 82 | ertr4d 8673 |
. . . . . . . . . 10
β’ ((π β§ π β βͺ π΅) β (πΌ(*πβπ½)π)( βphβπ½)((πΌ(*πβπ½)(π(*πβπ½)πΉ))(*πβπ½)πΌ)) |
84 | 63, 64, 83 | pcohtpy 24406 |
. . . . . . . . 9
β’ ((π β§ π β βͺ π΅) β (πΉ(*πβπ½)(πΌ(*πβπ½)π))( βphβπ½)(πΉ(*πβπ½)((πΌ(*πβπ½)(π(*πβπ½)πΉ))(*πβπ½)πΌ))) |
85 | 27, 13, 26, 69, 33, 70 | pcoass 24410 |
. . . . . . . . . 10
β’ ((π β§ π β βͺ π΅) β ((πΉ(*πβπ½)πΌ)(*πβπ½)π)( βphβπ½)(πΉ(*πβπ½)(πΌ(*πβπ½)π))) |
86 | 27, 13 | pco1 24401 |
. . . . . . . . . . . . 13
β’ ((π β§ π β βͺ π΅) β ((πΉ(*πβπ½)πΌ)β1) = (πΌβ1)) |
87 | 86, 33 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ ((π β§ π β βͺ π΅) β ((πΉ(*πβπ½)πΌ)β1) = (πβ0)) |
88 | 87, 76, 74 | pcohtpy 24406 |
. . . . . . . . . . 11
β’ ((π β§ π β βͺ π΅) β ((πΉ(*πβπ½)πΌ)(*πβπ½)π)( βphβπ½)(((0[,]1) Γ {(πΉβ0)})(*πβπ½)π)) |
89 | 66 | pcopt 24408 |
. . . . . . . . . . . 12
β’ ((π β (II Cn π½) β§ (πβ0) = (πΉβ0)) β (((0[,]1) Γ {(πΉβ0)})(*πβπ½)π)( βphβπ½)π) |
90 | 26, 32, 89 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ π β βͺ π΅) β (((0[,]1) Γ
{(πΉβ0)})(*πβπ½)π)( βphβπ½)π) |
91 | 61, 88, 90 | ertrd 8670 |
. . . . . . . . . 10
β’ ((π β§ π β βͺ π΅) β ((πΉ(*πβπ½)πΌ)(*πβπ½)π)( βphβπ½)π) |
92 | 61, 85, 91 | ertr3d 8672 |
. . . . . . . . 9
β’ ((π β§ π β βͺ π΅) β (πΉ(*πβπ½)(πΌ(*πβπ½)π))( βphβπ½)π) |
93 | 61, 84, 92 | ertr3d 8672 |
. . . . . . . 8
β’ ((π β§ π β βͺ π΅) β (πΉ(*πβπ½)((πΌ(*πβπ½)(π(*πβπ½)πΉ))(*πβπ½)πΌ))( βphβπ½)π) |
94 | 61, 93 | erthi 8705 |
. . . . . . 7
β’ ((π β§ π β βͺ π΅) β [(πΉ(*πβπ½)((πΌ(*πβπ½)(π(*πβπ½)πΉ))(*πβπ½)πΌ))]( βphβπ½) = [π]( βphβπ½)) |
95 | 94 | opeq2d 4841 |
. . . . . 6
β’ ((π β§ π β βͺ π΅) β β¨[(πΌ(*πβπ½)(π(*πβπ½)πΉ))]( βphβπ½), [(πΉ(*πβπ½)((πΌ(*πβπ½)(π(*πβπ½)πΉ))(*πβπ½)πΌ))]( βphβπ½)β© = β¨[(πΌ(*πβπ½)(π(*πβπ½)πΉ))]( βphβπ½), [π]( βphβπ½)β©) |
96 | 95 | mpteq2dva 5209 |
. . . . 5
β’ (π β (π β βͺ π΅ β¦ β¨[(πΌ(*πβπ½)(π(*πβπ½)πΉ))]( βphβπ½), [(πΉ(*πβπ½)((πΌ(*πβπ½)(π(*πβπ½)πΉ))(*πβπ½)πΌ))]( βphβπ½)β©) = (π β βͺ π΅ β¦ β¨[(πΌ(*πβπ½)(π(*πβπ½)πΉ))]( βphβπ½), [π]( βphβπ½)β©)) |
97 | 59, 96 | eqtrd 2773 |
. . . 4
β’ (π β ((β β βͺ
(Baseβπ) β¦
β¨[β](
βphβπ½), [(πΉ(*πβπ½)(β(*πβπ½)πΌ))]( βphβπ½)β©) β (π β βͺ π΅
β¦ (πΌ(*πβπ½)(π(*πβπ½)πΉ)))) = (π β βͺ π΅ β¦ β¨[(πΌ(*πβπ½)(π(*πβπ½)πΉ))]( βphβπ½), [π]( βphβπ½)β©)) |
98 | 97 | rneqd 5897 |
. . 3
β’ (π β ran ((β β βͺ
(Baseβπ) β¦
β¨[β](
βphβπ½), [(πΉ(*πβπ½)(β(*πβπ½)πΌ))]( βphβπ½)β©) β (π β βͺ π΅
β¦ (πΌ(*πβπ½)(π(*πβπ½)πΉ)))) = ran (π β βͺ π΅ β¦ β¨[(πΌ(*πβπ½)(π(*πβπ½)πΉ))]( βphβπ½), [π]( βphβπ½)β©)) |
99 | 7, 98 | eqtr4d 2776 |
. 2
β’ (π β β‘πΊ = ran ((β β βͺ
(Baseβπ) β¦
β¨[β](
βphβπ½), [(πΉ(*πβπ½)(β(*πβπ½)πΌ))]( βphβπ½)β©) β (π β βͺ π΅
β¦ (πΌ(*πβπ½)(π(*πβπ½)πΉ))))) |
100 | | rncoss 5931 |
. . 3
β’ ran
((β β βͺ (Baseβπ) β¦ β¨[β]( βphβπ½), [(πΉ(*πβπ½)(β(*πβπ½)πΌ))]( βphβπ½)β©) β (π β βͺ π΅
β¦ (πΌ(*πβπ½)(π(*πβπ½)πΉ)))) β ran (β β βͺ
(Baseβπ) β¦
β¨[β](
βphβπ½), [(πΉ(*πβπ½)(β(*πβπ½)πΌ))]( βphβπ½)β©) |
101 | | pi1xfrcnv.h |
. . 3
β’ π» = ran (β β βͺ
(Baseβπ) β¦
β¨[β](
βphβπ½), [(πΉ(*πβπ½)(β(*πβπ½)πΌ))]( βphβπ½)β©) |
102 | 100, 101 | sseqtrri 3985 |
. 2
β’ ran
((β β βͺ (Baseβπ) β¦ β¨[β]( βphβπ½), [(πΉ(*πβπ½)(β(*πβπ½)πΌ))]( βphβπ½)β©) β (π β βͺ π΅
β¦ (πΌ(*πβπ½)(π(*πβπ½)πΉ)))) β π» |
103 | 99, 102 | eqsstrdi 4002 |
1
β’ (π β β‘πΊ β π») |