Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . 4
β’ ((πΉ:π΄βΆπ΅ β§ π΄ β π) β π΄ β π) |
2 | 1 | mptexd 7226 |
. . 3
β’ ((πΉ:π΄βΆπ΅ β§ π΄ β π) β (π β π΄ β¦ (β‘πΉ β {(πΉβπ)})) β V) |
3 | | fundcmpsurinj.p |
. . . . . 6
β’ π = {π§ β£ βπ₯ β π΄ π§ = (β‘πΉ β {(πΉβπ₯)})} |
4 | 3 | setpreimafvex 46051 |
. . . . 5
β’ (π΄ β π β π β V) |
5 | 4 | adantl 483 |
. . . 4
β’ ((πΉ:π΄βΆπ΅ β§ π΄ β π) β π β V) |
6 | 5 | mptexd 7226 |
. . 3
β’ ((πΉ:π΄βΆπ΅ β§ π΄ β π) β (π¦ β π β¦ βͺ (πΉ β π¦)) β V) |
7 | | ffun 6721 |
. . . . 5
β’ (πΉ:π΄βΆπ΅ β Fun πΉ) |
8 | | funimaexg 6635 |
. . . . 5
β’ ((Fun
πΉ β§ π΄ β π) β (πΉ β π΄) β V) |
9 | 7, 8 | sylan 581 |
. . . 4
β’ ((πΉ:π΄βΆπ΅ β§ π΄ β π) β (πΉ β π΄) β V) |
10 | 9 | resiexd 7218 |
. . 3
β’ ((πΉ:π΄βΆπ΅ β§ π΄ β π) β ( I βΎ (πΉ β π΄)) β V) |
11 | 2, 6, 10 | 3jca 1129 |
. 2
β’ ((πΉ:π΄βΆπ΅ β§ π΄ β π) β ((π β π΄ β¦ (β‘πΉ β {(πΉβπ)})) β V β§ (π¦ β π β¦ βͺ (πΉ β π¦)) β V β§ ( I βΎ (πΉ β π΄)) β V)) |
12 | | ffn 6718 |
. . . . 5
β’ (πΉ:π΄βΆπ΅ β πΉ Fn π΄) |
13 | | fveq2 6892 |
. . . . . . . . 9
β’ (π = π₯ β (πΉβπ) = (πΉβπ₯)) |
14 | 13 | sneqd 4641 |
. . . . . . . 8
β’ (π = π₯ β {(πΉβπ)} = {(πΉβπ₯)}) |
15 | 14 | imaeq2d 6060 |
. . . . . . 7
β’ (π = π₯ β (β‘πΉ β {(πΉβπ)}) = (β‘πΉ β {(πΉβπ₯)})) |
16 | 15 | cbvmptv 5262 |
. . . . . 6
β’ (π β π΄ β¦ (β‘πΉ β {(πΉβπ)})) = (π₯ β π΄ β¦ (β‘πΉ β {(πΉβπ₯)})) |
17 | 3, 16 | fundcmpsurinjlem2 46067 |
. . . . 5
β’ ((πΉ Fn π΄ β§ π΄ β π) β (π β π΄ β¦ (β‘πΉ β {(πΉβπ)})):π΄βontoβπ) |
18 | 12, 17 | sylan 581 |
. . . 4
β’ ((πΉ:π΄βΆπ΅ β§ π΄ β π) β (π β π΄ β¦ (β‘πΉ β {(πΉβπ)})):π΄βontoβπ) |
19 | | eqid 2733 |
. . . . . 6
β’ (π¦ β π β¦ βͺ (πΉ β π¦)) = (π¦ β π β¦ βͺ (πΉ β π¦)) |
20 | 3, 19 | imasetpreimafvbij 46074 |
. . . . 5
β’ ((πΉ Fn π΄ β§ π΄ β π) β (π¦ β π β¦ βͺ (πΉ β π¦)):πβ1-1-ontoβ(πΉ β π΄)) |
21 | 12, 20 | sylan 581 |
. . . 4
β’ ((πΉ:π΄βΆπ΅ β§ π΄ β π) β (π¦ β π β¦ βͺ (πΉ β π¦)):πβ1-1-ontoβ(πΉ β π΄)) |
22 | | f1oi 6872 |
. . . . . 6
β’ ( I
βΎ (πΉ β π΄)):(πΉ β π΄)β1-1-ontoβ(πΉ β π΄) |
23 | | f1of1 6833 |
. . . . . 6
β’ (( I
βΎ (πΉ β π΄)):(πΉ β π΄)β1-1-ontoβ(πΉ β π΄) β ( I βΎ (πΉ β π΄)):(πΉ β π΄)β1-1β(πΉ β π΄)) |
24 | | fimass 6739 |
. . . . . . . 8
β’ (πΉ:π΄βΆπ΅ β (πΉ β π΄) β π΅) |
25 | | f1ss 6794 |
. . . . . . . 8
β’ ((( I
βΎ (πΉ β π΄)):(πΉ β π΄)β1-1β(πΉ β π΄) β§ (πΉ β π΄) β π΅) β ( I βΎ (πΉ β π΄)):(πΉ β π΄)β1-1βπ΅) |
26 | 24, 25 | sylan2 594 |
. . . . . . 7
β’ ((( I
βΎ (πΉ β π΄)):(πΉ β π΄)β1-1β(πΉ β π΄) β§ πΉ:π΄βΆπ΅) β ( I βΎ (πΉ β π΄)):(πΉ β π΄)β1-1βπ΅) |
27 | 26 | ex 414 |
. . . . . 6
β’ (( I
βΎ (πΉ β π΄)):(πΉ β π΄)β1-1β(πΉ β π΄) β (πΉ:π΄βΆπ΅ β ( I βΎ (πΉ β π΄)):(πΉ β π΄)β1-1βπ΅)) |
28 | 22, 23, 27 | mp2b 10 |
. . . . 5
β’ (πΉ:π΄βΆπ΅ β ( I βΎ (πΉ β π΄)):(πΉ β π΄)β1-1βπ΅) |
29 | 28 | adantr 482 |
. . . 4
β’ ((πΉ:π΄βΆπ΅ β§ π΄ β π) β ( I βΎ (πΉ β π΄)):(πΉ β π΄)β1-1βπ΅) |
30 | 18, 21, 29 | 3jca 1129 |
. . 3
β’ ((πΉ:π΄βΆπ΅ β§ π΄ β π) β ((π β π΄ β¦ (β‘πΉ β {(πΉβπ)})):π΄βontoβπ β§ (π¦ β π β¦ βͺ (πΉ β π¦)):πβ1-1-ontoβ(πΉ β π΄) β§ ( I βΎ (πΉ β π΄)):(πΉ β π΄)β1-1βπ΅)) |
31 | 12 | adantr 482 |
. . . . . . . . 9
β’ ((πΉ:π΄βΆπ΅ β§ π΄ β π) β πΉ Fn π΄) |
32 | | uniimaprimaeqfv 46050 |
. . . . . . . . 9
β’ ((πΉ Fn π΄ β§ π β π΄) β βͺ (πΉ β (β‘πΉ β {(πΉβπ)})) = (πΉβπ)) |
33 | 31, 32 | sylan 581 |
. . . . . . . 8
β’ (((πΉ:π΄βΆπ΅ β§ π΄ β π) β§ π β π΄) β βͺ (πΉ β (β‘πΉ β {(πΉβπ)})) = (πΉβπ)) |
34 | 33 | fveq2d 6896 |
. . . . . . 7
β’ (((πΉ:π΄βΆπ΅ β§ π΄ β π) β§ π β π΄) β (( I βΎ (πΉ β π΄))ββͺ (πΉ β (β‘πΉ β {(πΉβπ)}))) = (( I βΎ (πΉ β π΄))β(πΉβπ))) |
35 | 34 | mpteq2dva 5249 |
. . . . . 6
β’ ((πΉ:π΄βΆπ΅ β§ π΄ β π) β (π β π΄ β¦ (( I βΎ (πΉ β π΄))ββͺ (πΉ β (β‘πΉ β {(πΉβπ)})))) = (π β π΄ β¦ (( I βΎ (πΉ β π΄))β(πΉβπ)))) |
36 | | ffrn 6732 |
. . . . . . . . . 10
β’ (πΉ:π΄βΆπ΅ β πΉ:π΄βΆran πΉ) |
37 | 36 | adantr 482 |
. . . . . . . . 9
β’ ((πΉ:π΄βΆπ΅ β§ π΄ β π) β πΉ:π΄βΆran πΉ) |
38 | 37 | funfvima2d 7234 |
. . . . . . . 8
β’ (((πΉ:π΄βΆπ΅ β§ π΄ β π) β§ π β π΄) β (πΉβπ) β (πΉ β π΄)) |
39 | | fvresi 7171 |
. . . . . . . 8
β’ ((πΉβπ) β (πΉ β π΄) β (( I βΎ (πΉ β π΄))β(πΉβπ)) = (πΉβπ)) |
40 | 38, 39 | syl 17 |
. . . . . . 7
β’ (((πΉ:π΄βΆπ΅ β§ π΄ β π) β§ π β π΄) β (( I βΎ (πΉ β π΄))β(πΉβπ)) = (πΉβπ)) |
41 | 40 | mpteq2dva 5249 |
. . . . . 6
β’ ((πΉ:π΄βΆπ΅ β§ π΄ β π) β (π β π΄ β¦ (( I βΎ (πΉ β π΄))β(πΉβπ))) = (π β π΄ β¦ (πΉβπ))) |
42 | 35, 41 | eqtrd 2773 |
. . . . 5
β’ ((πΉ:π΄βΆπ΅ β§ π΄ β π) β (π β π΄ β¦ (( I βΎ (πΉ β π΄))ββͺ (πΉ β (β‘πΉ β {(πΉβπ)})))) = (π β π΄ β¦ (πΉβπ))) |
43 | 12 | ad2antrr 725 |
. . . . . . 7
β’ (((πΉ:π΄βΆπ΅ β§ π΄ β π) β§ π β π΄) β πΉ Fn π΄) |
44 | 1 | adantr 482 |
. . . . . . 7
β’ (((πΉ:π΄βΆπ΅ β§ π΄ β π) β§ π β π΄) β π΄ β π) |
45 | | simpr 486 |
. . . . . . 7
β’ (((πΉ:π΄βΆπ΅ β§ π΄ β π) β§ π β π΄) β π β π΄) |
46 | 3 | preimafvelsetpreimafv 46056 |
. . . . . . 7
β’ ((πΉ Fn π΄ β§ π΄ β π β§ π β π΄) β (β‘πΉ β {(πΉβπ)}) β π) |
47 | 43, 44, 45, 46 | syl3anc 1372 |
. . . . . 6
β’ (((πΉ:π΄βΆπ΅ β§ π΄ β π) β§ π β π΄) β (β‘πΉ β {(πΉβπ)}) β π) |
48 | | eqidd 2734 |
. . . . . 6
β’ ((πΉ:π΄βΆπ΅ β§ π΄ β π) β (π β π΄ β¦ (β‘πΉ β {(πΉβπ)})) = (π β π΄ β¦ (β‘πΉ β {(πΉβπ)}))) |
49 | | eqidd 2734 |
. . . . . 6
β’ ((πΉ:π΄βΆπ΅ β§ π΄ β π) β (π¦ β π β¦ (( I βΎ (πΉ β π΄))ββͺ (πΉ β π¦))) = (π¦ β π β¦ (( I βΎ (πΉ β π΄))ββͺ (πΉ β π¦)))) |
50 | | imaeq2 6056 |
. . . . . . . 8
β’ (π¦ = (β‘πΉ β {(πΉβπ)}) β (πΉ β π¦) = (πΉ β (β‘πΉ β {(πΉβπ)}))) |
51 | 50 | unieqd 4923 |
. . . . . . 7
β’ (π¦ = (β‘πΉ β {(πΉβπ)}) β βͺ
(πΉ β π¦) = βͺ
(πΉ β (β‘πΉ β {(πΉβπ)}))) |
52 | 51 | fveq2d 6896 |
. . . . . 6
β’ (π¦ = (β‘πΉ β {(πΉβπ)}) β (( I βΎ (πΉ β π΄))ββͺ (πΉ β π¦)) = (( I βΎ (πΉ β π΄))ββͺ (πΉ β (β‘πΉ β {(πΉβπ)})))) |
53 | 47, 48, 49, 52 | fmptco 7127 |
. . . . 5
β’ ((πΉ:π΄βΆπ΅ β§ π΄ β π) β ((π¦ β π β¦ (( I βΎ (πΉ β π΄))ββͺ (πΉ β π¦))) β (π β π΄ β¦ (β‘πΉ β {(πΉβπ)}))) = (π β π΄ β¦ (( I βΎ (πΉ β π΄))ββͺ (πΉ β (β‘πΉ β {(πΉβπ)}))))) |
54 | | dffn5 6951 |
. . . . . . 7
β’ (πΉ Fn π΄ β πΉ = (π β π΄ β¦ (πΉβπ))) |
55 | 12, 54 | sylib 217 |
. . . . . 6
β’ (πΉ:π΄βΆπ΅ β πΉ = (π β π΄ β¦ (πΉβπ))) |
56 | 55 | adantr 482 |
. . . . 5
β’ ((πΉ:π΄βΆπ΅ β§ π΄ β π) β πΉ = (π β π΄ β¦ (πΉβπ))) |
57 | 42, 53, 56 | 3eqtr4rd 2784 |
. . . 4
β’ ((πΉ:π΄βΆπ΅ β§ π΄ β π) β πΉ = ((π¦ β π β¦ (( I βΎ (πΉ β π΄))ββͺ (πΉ β π¦))) β (π β π΄ β¦ (β‘πΉ β {(πΉβπ)})))) |
58 | | f1of 6834 |
. . . . . . . . . 10
β’ (( I
βΎ (πΉ β π΄)):(πΉ β π΄)β1-1-ontoβ(πΉ β π΄) β ( I βΎ (πΉ β π΄)):(πΉ β π΄)βΆ(πΉ β π΄)) |
59 | 22, 58 | mp1i 13 |
. . . . . . . . 9
β’ (πΉ Fn π΄ β ( I βΎ (πΉ β π΄)):(πΉ β π΄)βΆ(πΉ β π΄)) |
60 | | fnima 6681 |
. . . . . . . . . . 11
β’ (πΉ Fn π΄ β (πΉ β π΄) = ran πΉ) |
61 | 60 | eqcomd 2739 |
. . . . . . . . . 10
β’ (πΉ Fn π΄ β ran πΉ = (πΉ β π΄)) |
62 | 61 | feq2d 6704 |
. . . . . . . . 9
β’ (πΉ Fn π΄ β (( I βΎ (πΉ β π΄)):ran πΉβΆ(πΉ β π΄) β ( I βΎ (πΉ β π΄)):(πΉ β π΄)βΆ(πΉ β π΄))) |
63 | 59, 62 | mpbird 257 |
. . . . . . . 8
β’ (πΉ Fn π΄ β ( I βΎ (πΉ β π΄)):ran πΉβΆ(πΉ β π΄)) |
64 | 3 | uniimaelsetpreimafv 46064 |
. . . . . . . 8
β’ ((πΉ Fn π΄ β§ π¦ β π) β βͺ (πΉ β π¦) β ran πΉ) |
65 | 63, 64 | cofmpt 7130 |
. . . . . . 7
β’ (πΉ Fn π΄ β (( I βΎ (πΉ β π΄)) β (π¦ β π β¦ βͺ (πΉ β π¦))) = (π¦ β π β¦ (( I βΎ (πΉ β π΄))ββͺ (πΉ β π¦)))) |
66 | 65 | eqcomd 2739 |
. . . . . 6
β’ (πΉ Fn π΄ β (π¦ β π β¦ (( I βΎ (πΉ β π΄))ββͺ (πΉ β π¦))) = (( I βΎ (πΉ β π΄)) β (π¦ β π β¦ βͺ (πΉ β π¦)))) |
67 | 31, 66 | syl 17 |
. . . . 5
β’ ((πΉ:π΄βΆπ΅ β§ π΄ β π) β (π¦ β π β¦ (( I βΎ (πΉ β π΄))ββͺ (πΉ β π¦))) = (( I βΎ (πΉ β π΄)) β (π¦ β π β¦ βͺ (πΉ β π¦)))) |
68 | 67 | coeq1d 5862 |
. . . 4
β’ ((πΉ:π΄βΆπ΅ β§ π΄ β π) β ((π¦ β π β¦ (( I βΎ (πΉ β π΄))ββͺ (πΉ β π¦))) β (π β π΄ β¦ (β‘πΉ β {(πΉβπ)}))) = ((( I βΎ (πΉ β π΄)) β (π¦ β π β¦ βͺ (πΉ β π¦))) β (π β π΄ β¦ (β‘πΉ β {(πΉβπ)})))) |
69 | 57, 68 | eqtrd 2773 |
. . 3
β’ ((πΉ:π΄βΆπ΅ β§ π΄ β π) β πΉ = ((( I βΎ (πΉ β π΄)) β (π¦ β π β¦ βͺ (πΉ β π¦))) β (π β π΄ β¦ (β‘πΉ β {(πΉβπ)})))) |
70 | 30, 69 | jca 513 |
. 2
β’ ((πΉ:π΄βΆπ΅ β§ π΄ β π) β (((π β π΄ β¦ (β‘πΉ β {(πΉβπ)})):π΄βontoβπ β§ (π¦ β π β¦ βͺ (πΉ β π¦)):πβ1-1-ontoβ(πΉ β π΄) β§ ( I βΎ (πΉ β π΄)):(πΉ β π΄)β1-1βπ΅) β§ πΉ = ((( I βΎ (πΉ β π΄)) β (π¦ β π β¦ βͺ (πΉ β π¦))) β (π β π΄ β¦ (β‘πΉ β {(πΉβπ)}))))) |
71 | | foeq1 6802 |
. . . . . 6
β’ (π = (π β π΄ β¦ (β‘πΉ β {(πΉβπ)})) β (π:π΄βontoβπ β (π β π΄ β¦ (β‘πΉ β {(πΉβπ)})):π΄βontoβπ)) |
72 | 71 | 3ad2ant1 1134 |
. . . . 5
β’ ((π = (π β π΄ β¦ (β‘πΉ β {(πΉβπ)})) β§ β = (π¦ β π β¦ βͺ (πΉ β π¦)) β§ π = ( I βΎ (πΉ β π΄))) β (π:π΄βontoβπ β (π β π΄ β¦ (β‘πΉ β {(πΉβπ)})):π΄βontoβπ)) |
73 | | f1oeq1 6822 |
. . . . . 6
β’ (β = (π¦ β π β¦ βͺ (πΉ β π¦)) β (β:πβ1-1-ontoβ(πΉ β π΄) β (π¦ β π β¦ βͺ (πΉ β π¦)):πβ1-1-ontoβ(πΉ β π΄))) |
74 | 73 | 3ad2ant2 1135 |
. . . . 5
β’ ((π = (π β π΄ β¦ (β‘πΉ β {(πΉβπ)})) β§ β = (π¦ β π β¦ βͺ (πΉ β π¦)) β§ π = ( I βΎ (πΉ β π΄))) β (β:πβ1-1-ontoβ(πΉ β π΄) β (π¦ β π β¦ βͺ (πΉ β π¦)):πβ1-1-ontoβ(πΉ β π΄))) |
75 | | f1eq1 6783 |
. . . . . 6
β’ (π = ( I βΎ (πΉ β π΄)) β (π:(πΉ β π΄)β1-1βπ΅ β ( I βΎ (πΉ β π΄)):(πΉ β π΄)β1-1βπ΅)) |
76 | 75 | 3ad2ant3 1136 |
. . . . 5
β’ ((π = (π β π΄ β¦ (β‘πΉ β {(πΉβπ)})) β§ β = (π¦ β π β¦ βͺ (πΉ β π¦)) β§ π = ( I βΎ (πΉ β π΄))) β (π:(πΉ β π΄)β1-1βπ΅ β ( I βΎ (πΉ β π΄)):(πΉ β π΄)β1-1βπ΅)) |
77 | 72, 74, 76 | 3anbi123d 1437 |
. . . 4
β’ ((π = (π β π΄ β¦ (β‘πΉ β {(πΉβπ)})) β§ β = (π¦ β π β¦ βͺ (πΉ β π¦)) β§ π = ( I βΎ (πΉ β π΄))) β ((π:π΄βontoβπ β§ β:πβ1-1-ontoβ(πΉ β π΄) β§ π:(πΉ β π΄)β1-1βπ΅) β ((π β π΄ β¦ (β‘πΉ β {(πΉβπ)})):π΄βontoβπ β§ (π¦ β π β¦ βͺ (πΉ β π¦)):πβ1-1-ontoβ(πΉ β π΄) β§ ( I βΎ (πΉ β π΄)):(πΉ β π΄)β1-1βπ΅))) |
78 | | simp3 1139 |
. . . . . . 7
β’ ((π = (π β π΄ β¦ (β‘πΉ β {(πΉβπ)})) β§ β = (π¦ β π β¦ βͺ (πΉ β π¦)) β§ π = ( I βΎ (πΉ β π΄))) β π = ( I βΎ (πΉ β π΄))) |
79 | | simp2 1138 |
. . . . . . 7
β’ ((π = (π β π΄ β¦ (β‘πΉ β {(πΉβπ)})) β§ β = (π¦ β π β¦ βͺ (πΉ β π¦)) β§ π = ( I βΎ (πΉ β π΄))) β β = (π¦ β π β¦ βͺ (πΉ β π¦))) |
80 | 78, 79 | coeq12d 5865 |
. . . . . 6
β’ ((π = (π β π΄ β¦ (β‘πΉ β {(πΉβπ)})) β§ β = (π¦ β π β¦ βͺ (πΉ β π¦)) β§ π = ( I βΎ (πΉ β π΄))) β (π β β) = (( I βΎ (πΉ β π΄)) β (π¦ β π β¦ βͺ (πΉ β π¦)))) |
81 | | simp1 1137 |
. . . . . 6
β’ ((π = (π β π΄ β¦ (β‘πΉ β {(πΉβπ)})) β§ β = (π¦ β π β¦ βͺ (πΉ β π¦)) β§ π = ( I βΎ (πΉ β π΄))) β π = (π β π΄ β¦ (β‘πΉ β {(πΉβπ)}))) |
82 | 80, 81 | coeq12d 5865 |
. . . . 5
β’ ((π = (π β π΄ β¦ (β‘πΉ β {(πΉβπ)})) β§ β = (π¦ β π β¦ βͺ (πΉ β π¦)) β§ π = ( I βΎ (πΉ β π΄))) β ((π β β) β π) = ((( I βΎ (πΉ β π΄)) β (π¦ β π β¦ βͺ (πΉ β π¦))) β (π β π΄ β¦ (β‘πΉ β {(πΉβπ)})))) |
83 | 82 | eqeq2d 2744 |
. . . 4
β’ ((π = (π β π΄ β¦ (β‘πΉ β {(πΉβπ)})) β§ β = (π¦ β π β¦ βͺ (πΉ β π¦)) β§ π = ( I βΎ (πΉ β π΄))) β (πΉ = ((π β β) β π) β πΉ = ((( I βΎ (πΉ β π΄)) β (π¦ β π β¦ βͺ (πΉ β π¦))) β (π β π΄ β¦ (β‘πΉ β {(πΉβπ)}))))) |
84 | 77, 83 | anbi12d 632 |
. . 3
β’ ((π = (π β π΄ β¦ (β‘πΉ β {(πΉβπ)})) β§ β = (π¦ β π β¦ βͺ (πΉ β π¦)) β§ π = ( I βΎ (πΉ β π΄))) β (((π:π΄βontoβπ β§ β:πβ1-1-ontoβ(πΉ β π΄) β§ π:(πΉ β π΄)β1-1βπ΅) β§ πΉ = ((π β β) β π)) β (((π β π΄ β¦ (β‘πΉ β {(πΉβπ)})):π΄βontoβπ β§ (π¦ β π β¦ βͺ (πΉ β π¦)):πβ1-1-ontoβ(πΉ β π΄) β§ ( I βΎ (πΉ β π΄)):(πΉ β π΄)β1-1βπ΅) β§ πΉ = ((( I βΎ (πΉ β π΄)) β (π¦ β π β¦ βͺ (πΉ β π¦))) β (π β π΄ β¦ (β‘πΉ β {(πΉβπ)})))))) |
85 | 84 | spc3egv 3594 |
. 2
β’ (((π β π΄ β¦ (β‘πΉ β {(πΉβπ)})) β V β§ (π¦ β π β¦ βͺ (πΉ β π¦)) β V β§ ( I βΎ (πΉ β π΄)) β V) β ((((π β π΄ β¦ (β‘πΉ β {(πΉβπ)})):π΄βontoβπ β§ (π¦ β π β¦ βͺ (πΉ β π¦)):πβ1-1-ontoβ(πΉ β π΄) β§ ( I βΎ (πΉ β π΄)):(πΉ β π΄)β1-1βπ΅) β§ πΉ = ((( I βΎ (πΉ β π΄)) β (π¦ β π β¦ βͺ (πΉ β π¦))) β (π β π΄ β¦ (β‘πΉ β {(πΉβπ)})))) β βπβββπ((π:π΄βontoβπ β§ β:πβ1-1-ontoβ(πΉ β π΄) β§ π:(πΉ β π΄)β1-1βπ΅) β§ πΉ = ((π β β) β π)))) |
86 | 11, 70, 85 | sylc 65 |
1
β’ ((πΉ:π΄βΆπ΅ β§ π΄ β π) β βπβββπ((π:π΄βontoβπ β§ β:πβ1-1-ontoβ(πΉ β π΄) β§ π:(πΉ β π΄)β1-1βπ΅) β§ πΉ = ((π β β) β π))) |