Step | Hyp | Ref
| Expression |
1 | | qtophmeo.2 |
. . . . 5
β’ (π β π½ β (TopOnβπ)) |
2 | | qtophmeo.3 |
. . . . 5
β’ (π β πΉ:πβontoβπ) |
3 | | qtophmeo.4 |
. . . . . . 7
β’ (π β πΊ:πβontoβπ) |
4 | | fofn 6759 |
. . . . . . 7
β’ (πΊ:πβontoβπ β πΊ Fn π) |
5 | 3, 4 | syl 17 |
. . . . . 6
β’ (π β πΊ Fn π) |
6 | | qtopid 23072 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΊ Fn π) β πΊ β (π½ Cn (π½ qTop πΊ))) |
7 | 1, 5, 6 | syl2anc 585 |
. . . . 5
β’ (π β πΊ β (π½ Cn (π½ qTop πΊ))) |
8 | | df-3an 1090 |
. . . . . 6
β’ ((π₯ β π β§ π¦ β π β§ (πΉβπ₯) = (πΉβπ¦)) β ((π₯ β π β§ π¦ β π) β§ (πΉβπ₯) = (πΉβπ¦))) |
9 | | qtophmeo.5 |
. . . . . . . 8
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ((πΉβπ₯) = (πΉβπ¦) β (πΊβπ₯) = (πΊβπ¦))) |
10 | 9 | biimpd 228 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ((πΉβπ₯) = (πΉβπ¦) β (πΊβπ₯) = (πΊβπ¦))) |
11 | 10 | impr 456 |
. . . . . 6
β’ ((π β§ ((π₯ β π β§ π¦ β π) β§ (πΉβπ₯) = (πΉβπ¦))) β (πΊβπ₯) = (πΊβπ¦)) |
12 | 8, 11 | sylan2b 595 |
. . . . 5
β’ ((π β§ (π₯ β π β§ π¦ β π β§ (πΉβπ₯) = (πΉβπ¦))) β (πΊβπ₯) = (πΊβπ¦)) |
13 | 1, 2, 7, 12 | qtopeu 23083 |
. . . 4
β’ (π β β!π β ((π½ qTop πΉ) Cn (π½ qTop πΊ))πΊ = (π β πΉ)) |
14 | | reurex 3356 |
. . . 4
β’
(β!π β
((π½ qTop πΉ) Cn (π½ qTop πΊ))πΊ = (π β πΉ) β βπ β ((π½ qTop πΉ) Cn (π½ qTop πΊ))πΊ = (π β πΉ)) |
15 | 13, 14 | syl 17 |
. . 3
β’ (π β βπ β ((π½ qTop πΉ) Cn (π½ qTop πΊ))πΊ = (π β πΉ)) |
16 | | simprl 770 |
. . . 4
β’ ((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β π β ((π½ qTop πΉ) Cn (π½ qTop πΊ))) |
17 | | fofn 6759 |
. . . . . . . . . 10
β’ (πΉ:πβontoβπ β πΉ Fn π) |
18 | 2, 17 | syl 17 |
. . . . . . . . 9
β’ (π β πΉ Fn π) |
19 | | qtopid 23072 |
. . . . . . . . 9
β’ ((π½ β (TopOnβπ) β§ πΉ Fn π) β πΉ β (π½ Cn (π½ qTop πΉ))) |
20 | 1, 18, 19 | syl2anc 585 |
. . . . . . . 8
β’ (π β πΉ β (π½ Cn (π½ qTop πΉ))) |
21 | | df-3an 1090 |
. . . . . . . . 9
β’ ((π₯ β π β§ π¦ β π β§ (πΊβπ₯) = (πΊβπ¦)) β ((π₯ β π β§ π¦ β π) β§ (πΊβπ₯) = (πΊβπ¦))) |
22 | 9 | biimprd 248 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ((πΊβπ₯) = (πΊβπ¦) β (πΉβπ₯) = (πΉβπ¦))) |
23 | 22 | impr 456 |
. . . . . . . . 9
β’ ((π β§ ((π₯ β π β§ π¦ β π) β§ (πΊβπ₯) = (πΊβπ¦))) β (πΉβπ₯) = (πΉβπ¦)) |
24 | 21, 23 | sylan2b 595 |
. . . . . . . 8
β’ ((π β§ (π₯ β π β§ π¦ β π β§ (πΊβπ₯) = (πΊβπ¦))) β (πΉβπ₯) = (πΉβπ¦)) |
25 | 1, 3, 20, 24 | qtopeu 23083 |
. . . . . . 7
β’ (π β β!π β ((π½ qTop πΊ) Cn (π½ qTop πΉ))πΉ = (π β πΊ)) |
26 | 25 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β β!π β ((π½ qTop πΊ) Cn (π½ qTop πΉ))πΉ = (π β πΊ)) |
27 | | reurex 3356 |
. . . . . 6
β’
(β!π β
((π½ qTop πΊ) Cn (π½ qTop πΉ))πΉ = (π β πΊ) β βπ β ((π½ qTop πΊ) Cn (π½ qTop πΉ))πΉ = (π β πΊ)) |
28 | 26, 27 | syl 17 |
. . . . 5
β’ ((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β βπ β ((π½ qTop πΊ) Cn (π½ qTop πΉ))πΉ = (π β πΊ)) |
29 | | qtoptopon 23071 |
. . . . . . . . . 10
β’ ((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β (π½ qTop πΉ) β (TopOnβπ)) |
30 | 1, 2, 29 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (π½ qTop πΉ) β (TopOnβπ)) |
31 | 30 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β§ (π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ πΉ = (π β πΊ))) β (π½ qTop πΉ) β (TopOnβπ)) |
32 | | qtoptopon 23071 |
. . . . . . . . . 10
β’ ((π½ β (TopOnβπ) β§ πΊ:πβontoβπ) β (π½ qTop πΊ) β (TopOnβπ)) |
33 | 1, 3, 32 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (π½ qTop πΊ) β (TopOnβπ)) |
34 | 33 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β§ (π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ πΉ = (π β πΊ))) β (π½ qTop πΊ) β (TopOnβπ)) |
35 | | simplrl 776 |
. . . . . . . 8
β’ (((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β§ (π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ πΉ = (π β πΊ))) β π β ((π½ qTop πΉ) Cn (π½ qTop πΊ))) |
36 | | cnf2 22616 |
. . . . . . . 8
β’ (((π½ qTop πΉ) β (TopOnβπ) β§ (π½ qTop πΊ) β (TopOnβπ) β§ π β ((π½ qTop πΉ) Cn (π½ qTop πΊ))) β π:πβΆπ) |
37 | 31, 34, 35, 36 | syl3anc 1372 |
. . . . . . 7
β’ (((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β§ (π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ πΉ = (π β πΊ))) β π:πβΆπ) |
38 | | simprl 770 |
. . . . . . . 8
β’ (((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β§ (π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ πΉ = (π β πΊ))) β π β ((π½ qTop πΊ) Cn (π½ qTop πΉ))) |
39 | | cnf2 22616 |
. . . . . . . 8
β’ (((π½ qTop πΊ) β (TopOnβπ) β§ (π½ qTop πΉ) β (TopOnβπ) β§ π β ((π½ qTop πΊ) Cn (π½ qTop πΉ))) β π:πβΆπ) |
40 | 34, 31, 38, 39 | syl3anc 1372 |
. . . . . . 7
β’ (((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β§ (π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ πΉ = (π β πΊ))) β π:πβΆπ) |
41 | | coeq1 5814 |
. . . . . . . . 9
β’ (β = (π β π) β (β β πΉ) = ((π β π) β πΉ)) |
42 | 41 | eqeq2d 2744 |
. . . . . . . 8
β’ (β = (π β π) β (πΉ = (β β πΉ) β πΉ = ((π β π) β πΉ))) |
43 | | coeq1 5814 |
. . . . . . . . 9
β’ (β = ( I βΎ π) β (β β πΉ) = (( I βΎ π) β πΉ)) |
44 | 43 | eqeq2d 2744 |
. . . . . . . 8
β’ (β = ( I βΎ π) β (πΉ = (β β πΉ) β πΉ = (( I βΎ π) β πΉ))) |
45 | | simpr3 1197 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π β§ π¦ β π β§ (πΉβπ₯) = (πΉβπ¦))) β (πΉβπ₯) = (πΉβπ¦)) |
46 | 1, 2, 20, 45 | qtopeu 23083 |
. . . . . . . . 9
β’ (π β β!β β ((π½ qTop πΉ) Cn (π½ qTop πΉ))πΉ = (β β πΉ)) |
47 | 46 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β§ (π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ πΉ = (π β πΊ))) β β!β β ((π½ qTop πΉ) Cn (π½ qTop πΉ))πΉ = (β β πΉ)) |
48 | | cnco 22633 |
. . . . . . . . 9
β’ ((π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ π β ((π½ qTop πΊ) Cn (π½ qTop πΉ))) β (π β π) β ((π½ qTop πΉ) Cn (π½ qTop πΉ))) |
49 | 35, 38, 48 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β§ (π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ πΉ = (π β πΊ))) β (π β π) β ((π½ qTop πΉ) Cn (π½ qTop πΉ))) |
50 | | idcn 22624 |
. . . . . . . . . 10
β’ ((π½ qTop πΉ) β (TopOnβπ) β ( I βΎ π) β ((π½ qTop πΉ) Cn (π½ qTop πΉ))) |
51 | 30, 50 | syl 17 |
. . . . . . . . 9
β’ (π β ( I βΎ π) β ((π½ qTop πΉ) Cn (π½ qTop πΉ))) |
52 | 51 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β§ (π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ πΉ = (π β πΊ))) β ( I βΎ π) β ((π½ qTop πΉ) Cn (π½ qTop πΉ))) |
53 | | simprr 772 |
. . . . . . . . . 10
β’ (((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β§ (π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ πΉ = (π β πΊ))) β πΉ = (π β πΊ)) |
54 | | simplrr 777 |
. . . . . . . . . . 11
β’ (((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β§ (π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ πΉ = (π β πΊ))) β πΊ = (π β πΉ)) |
55 | 54 | coeq2d 5819 |
. . . . . . . . . 10
β’ (((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β§ (π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ πΉ = (π β πΊ))) β (π β πΊ) = (π β (π β πΉ))) |
56 | 53, 55 | eqtrd 2773 |
. . . . . . . . 9
β’ (((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β§ (π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ πΉ = (π β πΊ))) β πΉ = (π β (π β πΉ))) |
57 | | coass 6218 |
. . . . . . . . 9
β’ ((π β π) β πΉ) = (π β (π β πΉ)) |
58 | 56, 57 | eqtr4di 2791 |
. . . . . . . 8
β’ (((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β§ (π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ πΉ = (π β πΊ))) β πΉ = ((π β π) β πΉ)) |
59 | | fof 6757 |
. . . . . . . . . . . 12
β’ (πΉ:πβontoβπ β πΉ:πβΆπ) |
60 | 2, 59 | syl 17 |
. . . . . . . . . . 11
β’ (π β πΉ:πβΆπ) |
61 | 60 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β§ (π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ πΉ = (π β πΊ))) β πΉ:πβΆπ) |
62 | | fcoi2 6718 |
. . . . . . . . . 10
β’ (πΉ:πβΆπ β (( I βΎ π) β πΉ) = πΉ) |
63 | 61, 62 | syl 17 |
. . . . . . . . 9
β’ (((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β§ (π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ πΉ = (π β πΊ))) β (( I βΎ π) β πΉ) = πΉ) |
64 | 63 | eqcomd 2739 |
. . . . . . . 8
β’ (((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β§ (π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ πΉ = (π β πΊ))) β πΉ = (( I βΎ π) β πΉ)) |
65 | 42, 44, 47, 49, 52, 58, 64 | reu2eqd 3695 |
. . . . . . 7
β’ (((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β§ (π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ πΉ = (π β πΊ))) β (π β π) = ( I βΎ π)) |
66 | | coeq1 5814 |
. . . . . . . . 9
β’ (β = (π β π) β (β β πΊ) = ((π β π) β πΊ)) |
67 | 66 | eqeq2d 2744 |
. . . . . . . 8
β’ (β = (π β π) β (πΊ = (β β πΊ) β πΊ = ((π β π) β πΊ))) |
68 | | coeq1 5814 |
. . . . . . . . 9
β’ (β = ( I βΎ π) β (β β πΊ) = (( I βΎ π) β πΊ)) |
69 | 68 | eqeq2d 2744 |
. . . . . . . 8
β’ (β = ( I βΎ π) β (πΊ = (β β πΊ) β πΊ = (( I βΎ π) β πΊ))) |
70 | | simpr3 1197 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π β§ π¦ β π β§ (πΊβπ₯) = (πΊβπ¦))) β (πΊβπ₯) = (πΊβπ¦)) |
71 | 1, 3, 7, 70 | qtopeu 23083 |
. . . . . . . . 9
β’ (π β β!β β ((π½ qTop πΊ) Cn (π½ qTop πΊ))πΊ = (β β πΊ)) |
72 | 71 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β§ (π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ πΉ = (π β πΊ))) β β!β β ((π½ qTop πΊ) Cn (π½ qTop πΊ))πΊ = (β β πΊ)) |
73 | | cnco 22633 |
. . . . . . . . 9
β’ ((π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ π β ((π½ qTop πΉ) Cn (π½ qTop πΊ))) β (π β π) β ((π½ qTop πΊ) Cn (π½ qTop πΊ))) |
74 | 38, 35, 73 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β§ (π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ πΉ = (π β πΊ))) β (π β π) β ((π½ qTop πΊ) Cn (π½ qTop πΊ))) |
75 | | idcn 22624 |
. . . . . . . . . 10
β’ ((π½ qTop πΊ) β (TopOnβπ) β ( I βΎ π) β ((π½ qTop πΊ) Cn (π½ qTop πΊ))) |
76 | 33, 75 | syl 17 |
. . . . . . . . 9
β’ (π β ( I βΎ π) β ((π½ qTop πΊ) Cn (π½ qTop πΊ))) |
77 | 76 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β§ (π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ πΉ = (π β πΊ))) β ( I βΎ π) β ((π½ qTop πΊ) Cn (π½ qTop πΊ))) |
78 | 53 | coeq2d 5819 |
. . . . . . . . . 10
β’ (((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β§ (π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ πΉ = (π β πΊ))) β (π β πΉ) = (π β (π β πΊ))) |
79 | 54, 78 | eqtrd 2773 |
. . . . . . . . 9
β’ (((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β§ (π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ πΉ = (π β πΊ))) β πΊ = (π β (π β πΊ))) |
80 | | coass 6218 |
. . . . . . . . 9
β’ ((π β π) β πΊ) = (π β (π β πΊ)) |
81 | 79, 80 | eqtr4di 2791 |
. . . . . . . 8
β’ (((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β§ (π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ πΉ = (π β πΊ))) β πΊ = ((π β π) β πΊ)) |
82 | | fof 6757 |
. . . . . . . . . . . 12
β’ (πΊ:πβontoβπ β πΊ:πβΆπ) |
83 | 3, 82 | syl 17 |
. . . . . . . . . . 11
β’ (π β πΊ:πβΆπ) |
84 | 83 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β§ (π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ πΉ = (π β πΊ))) β πΊ:πβΆπ) |
85 | | fcoi2 6718 |
. . . . . . . . . 10
β’ (πΊ:πβΆπ β (( I βΎ π) β πΊ) = πΊ) |
86 | 84, 85 | syl 17 |
. . . . . . . . 9
β’ (((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β§ (π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ πΉ = (π β πΊ))) β (( I βΎ π) β πΊ) = πΊ) |
87 | 86 | eqcomd 2739 |
. . . . . . . 8
β’ (((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β§ (π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ πΉ = (π β πΊ))) β πΊ = (( I βΎ π) β πΊ)) |
88 | 67, 69, 72, 74, 77, 81, 87 | reu2eqd 3695 |
. . . . . . 7
β’ (((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β§ (π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ πΉ = (π β πΊ))) β (π β π) = ( I βΎ π)) |
89 | 37, 40, 65, 88 | 2fcoidinvd 7242 |
. . . . . 6
β’ (((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β§ (π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ πΉ = (π β πΊ))) β β‘π = π) |
90 | 89, 38 | eqeltrd 2834 |
. . . . 5
β’ (((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β§ (π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)) β§ πΉ = (π β πΊ))) β β‘π β ((π½ qTop πΊ) Cn (π½ qTop πΉ))) |
91 | 28, 90 | rexlimddv 3155 |
. . . 4
β’ ((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β β‘π β ((π½ qTop πΊ) Cn (π½ qTop πΉ))) |
92 | | ishmeo 23126 |
. . . 4
β’ (π β ((π½ qTop πΉ)Homeo(π½ qTop πΊ)) β (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ β‘π β ((π½ qTop πΊ) Cn (π½ qTop πΉ)))) |
93 | 16, 91, 92 | sylanbrc 584 |
. . 3
β’ ((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β π β ((π½ qTop πΉ)Homeo(π½ qTop πΊ))) |
94 | | simprr 772 |
. . 3
β’ ((π β§ (π β ((π½ qTop πΉ) Cn (π½ qTop πΊ)) β§ πΊ = (π β πΉ))) β πΊ = (π β πΉ)) |
95 | 15, 93, 94 | reximssdv 3166 |
. 2
β’ (π β βπ β ((π½ qTop πΉ)Homeo(π½ qTop πΊ))πΊ = (π β πΉ)) |
96 | | eqtr2 2757 |
. . . 4
β’ ((πΊ = (π β πΉ) β§ πΊ = (π β πΉ)) β (π β πΉ) = (π β πΉ)) |
97 | 2 | adantr 482 |
. . . . 5
β’ ((π β§ (π β ((π½ qTop πΉ)Homeo(π½ qTop πΊ)) β§ π β ((π½ qTop πΉ)Homeo(π½ qTop πΊ)))) β πΉ:πβontoβπ) |
98 | 30 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β ((π½ qTop πΉ)Homeo(π½ qTop πΊ)) β§ π β ((π½ qTop πΉ)Homeo(π½ qTop πΊ)))) β (π½ qTop πΉ) β (TopOnβπ)) |
99 | 33 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β ((π½ qTop πΉ)Homeo(π½ qTop πΊ)) β§ π β ((π½ qTop πΉ)Homeo(π½ qTop πΊ)))) β (π½ qTop πΊ) β (TopOnβπ)) |
100 | | simprl 770 |
. . . . . . 7
β’ ((π β§ (π β ((π½ qTop πΉ)Homeo(π½ qTop πΊ)) β§ π β ((π½ qTop πΉ)Homeo(π½ qTop πΊ)))) β π β ((π½ qTop πΉ)Homeo(π½ qTop πΊ))) |
101 | | hmeof1o2 23130 |
. . . . . . 7
β’ (((π½ qTop πΉ) β (TopOnβπ) β§ (π½ qTop πΊ) β (TopOnβπ) β§ π β ((π½ qTop πΉ)Homeo(π½ qTop πΊ))) β π:πβ1-1-ontoβπ) |
102 | 98, 99, 100, 101 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ (π β ((π½ qTop πΉ)Homeo(π½ qTop πΊ)) β§ π β ((π½ qTop πΉ)Homeo(π½ qTop πΊ)))) β π:πβ1-1-ontoβπ) |
103 | | f1ofn 6786 |
. . . . . 6
β’ (π:πβ1-1-ontoβπ β π Fn π) |
104 | 102, 103 | syl 17 |
. . . . 5
β’ ((π β§ (π β ((π½ qTop πΉ)Homeo(π½ qTop πΊ)) β§ π β ((π½ qTop πΉ)Homeo(π½ qTop πΊ)))) β π Fn π) |
105 | | simprr 772 |
. . . . . . 7
β’ ((π β§ (π β ((π½ qTop πΉ)Homeo(π½ qTop πΊ)) β§ π β ((π½ qTop πΉ)Homeo(π½ qTop πΊ)))) β π β ((π½ qTop πΉ)Homeo(π½ qTop πΊ))) |
106 | | hmeof1o2 23130 |
. . . . . . 7
β’ (((π½ qTop πΉ) β (TopOnβπ) β§ (π½ qTop πΊ) β (TopOnβπ) β§ π β ((π½ qTop πΉ)Homeo(π½ qTop πΊ))) β π:πβ1-1-ontoβπ) |
107 | 98, 99, 105, 106 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ (π β ((π½ qTop πΉ)Homeo(π½ qTop πΊ)) β§ π β ((π½ qTop πΉ)Homeo(π½ qTop πΊ)))) β π:πβ1-1-ontoβπ) |
108 | | f1ofn 6786 |
. . . . . 6
β’ (π:πβ1-1-ontoβπ β π Fn π) |
109 | 107, 108 | syl 17 |
. . . . 5
β’ ((π β§ (π β ((π½ qTop πΉ)Homeo(π½ qTop πΊ)) β§ π β ((π½ qTop πΉ)Homeo(π½ qTop πΊ)))) β π Fn π) |
110 | | cocan2 7239 |
. . . . 5
β’ ((πΉ:πβontoβπ β§ π Fn π β§ π Fn π) β ((π β πΉ) = (π β πΉ) β π = π)) |
111 | 97, 104, 109, 110 | syl3anc 1372 |
. . . 4
β’ ((π β§ (π β ((π½ qTop πΉ)Homeo(π½ qTop πΊ)) β§ π β ((π½ qTop πΉ)Homeo(π½ qTop πΊ)))) β ((π β πΉ) = (π β πΉ) β π = π)) |
112 | 96, 111 | imbitrid 243 |
. . 3
β’ ((π β§ (π β ((π½ qTop πΉ)Homeo(π½ qTop πΊ)) β§ π β ((π½ qTop πΉ)Homeo(π½ qTop πΊ)))) β ((πΊ = (π β πΉ) β§ πΊ = (π β πΉ)) β π = π)) |
113 | 112 | ralrimivva 3194 |
. 2
β’ (π β βπ β ((π½ qTop πΉ)Homeo(π½ qTop πΊ))βπ β ((π½ qTop πΉ)Homeo(π½ qTop πΊ))((πΊ = (π β πΉ) β§ πΊ = (π β πΉ)) β π = π)) |
114 | | coeq1 5814 |
. . . 4
β’ (π = π β (π β πΉ) = (π β πΉ)) |
115 | 114 | eqeq2d 2744 |
. . 3
β’ (π = π β (πΊ = (π β πΉ) β πΊ = (π β πΉ))) |
116 | 115 | reu4 3690 |
. 2
β’
(β!π β
((π½ qTop πΉ)Homeo(π½ qTop πΊ))πΊ = (π β πΉ) β (βπ β ((π½ qTop πΉ)Homeo(π½ qTop πΊ))πΊ = (π β πΉ) β§ βπ β ((π½ qTop πΉ)Homeo(π½ qTop πΊ))βπ β ((π½ qTop πΉ)Homeo(π½ qTop πΊ))((πΊ = (π β πΉ) β§ πΊ = (π β πΉ)) β π = π))) |
117 | 95, 113, 116 | sylanbrc 584 |
1
β’ (π β β!π β ((π½ qTop πΉ)Homeo(π½ qTop πΊ))πΊ = (π β πΉ)) |