Step | Hyp | Ref
| Expression |
1 | | f1f 6784 |
. . . . 5
β’ (πΉ:π΄β1-1βπ΅ β πΉ:π΄βΆπ΅) |
2 | | fex2 7920 |
. . . . 5
β’ ((πΉ:π΄βΆπ΅ β§ π΄ β π β§ π΅ β π) β πΉ β V) |
3 | 1, 2 | syl3an1 1163 |
. . . 4
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β πΉ β V) |
4 | | f1stres 7995 |
. . . . 5
β’
(1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})):((π΅ β ran πΉ) Γ {π« βͺ ran π΄})βΆ(π΅ β ran πΉ) |
5 | | difexg 5326 |
. . . . . . 7
β’ (π΅ β π β (π΅ β ran πΉ) β V) |
6 | 5 | 3ad2ant3 1135 |
. . . . . 6
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β (π΅ β ran πΉ) β V) |
7 | | snex 5430 |
. . . . . 6
β’
{π« βͺ ran π΄} β V |
8 | | xpexg 7733 |
. . . . . 6
β’ (((π΅ β ran πΉ) β V β§ {π« βͺ ran π΄} β V) β ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}) β V) |
9 | 6, 7, 8 | sylancl 586 |
. . . . 5
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}) β V) |
10 | | fex2 7920 |
. . . . 5
β’
(((1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})):((π΅ β ran πΉ) Γ {π« βͺ ran π΄})βΆ(π΅ β ran πΉ) β§ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}) β V β§ (π΅ β ran πΉ) β V) β (1st βΎ
((π΅ β ran πΉ) Γ {π« βͺ ran π΄})) β V) |
11 | 4, 9, 6, 10 | mp3an2i 1466 |
. . . 4
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})) β V) |
12 | | unexg 7732 |
. . . 4
β’ ((πΉ β V β§ (1st
βΎ ((π΅ β ran
πΉ) Γ {π« βͺ ran π΄})) β V) β (πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) β V) |
13 | 3, 11, 12 | syl2anc 584 |
. . 3
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β (πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) β V) |
14 | | cnvexg 7911 |
. . 3
β’ ((πΉ βͺ (1st βΎ
((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) β V β β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) β V) |
15 | 13, 14 | syl 17 |
. 2
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) β V) |
16 | | eqid 2732 |
. . . . . . 7
β’ β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) = β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) |
17 | 16 | domss2 9132 |
. . . . . 6
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β (β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))):π΅β1-1-ontoβran
β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) β§ π΄ β ran β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) β§ (β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) β πΉ) = ( I βΎ π΄))) |
18 | 17 | simp1d 1142 |
. . . . 5
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))):π΅β1-1-ontoβran
β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})))) |
19 | | f1of1 6829 |
. . . . 5
β’ (β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))):π΅β1-1-ontoβran
β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) β β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))):π΅β1-1βran β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})))) |
20 | 18, 19 | syl 17 |
. . . 4
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))):π΅β1-1βran β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})))) |
21 | | ssv 4005 |
. . . 4
β’ ran β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) β V |
22 | | f1ss 6790 |
. . . 4
β’ ((β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))):π΅β1-1βran β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) β§ ran β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) β V) β β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))):π΅β1-1βV) |
23 | 20, 21, 22 | sylancl 586 |
. . 3
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))):π΅β1-1βV) |
24 | 17 | simp3d 1144 |
. . 3
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β (β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) β πΉ) = ( I βΎ π΄)) |
25 | 23, 24 | jca 512 |
. 2
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β (β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))):π΅β1-1βV β§ (β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) β πΉ) = ( I βΎ π΄))) |
26 | | f1eq1 6779 |
. . 3
β’ (π = β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) β (π:π΅β1-1βV β β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))):π΅β1-1βV)) |
27 | | coeq1 5855 |
. . . 4
β’ (π = β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) β (π β πΉ) = (β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) β πΉ)) |
28 | 27 | eqeq1d 2734 |
. . 3
β’ (π = β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) β ((π β πΉ) = ( I βΎ π΄) β (β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) β πΉ) = ( I βΎ π΄))) |
29 | 26, 28 | anbi12d 631 |
. 2
β’ (π = β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) β ((π:π΅β1-1βV β§ (π β πΉ) = ( I βΎ π΄)) β (β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))):π΅β1-1βV β§ (β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) β πΉ) = ( I βΎ π΄)))) |
30 | 15, 25, 29 | spcedv 3588 |
1
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β βπ(π:π΅β1-1βV β§ (π β πΉ) = ( I βΎ π΄))) |