Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > txhmeo | Unicode version |
Description: Lift a pair of homeomorphisms on the factors to a homeomorphism of product topologies. (Contributed by Mario Carneiro, 2-Sep-2015.) |
Ref | Expression |
---|---|
txhmeo.1 | |
txhmeo.2 | |
txhmeo.3 | |
txhmeo.4 |
Ref | Expression |
---|---|
txhmeo |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | txhmeo.3 | . . . . . 6 | |
2 | hmeocn 12801 | . . . . . 6 | |
3 | 1, 2 | syl 14 | . . . . 5 |
4 | cntop1 12697 | . . . . 5 | |
5 | 3, 4 | syl 14 | . . . 4 |
6 | txhmeo.1 | . . . . 5 | |
7 | 6 | toptopon 12512 | . . . 4 TopOn |
8 | 5, 7 | sylib 121 | . . 3 TopOn |
9 | txhmeo.4 | . . . . . 6 | |
10 | hmeocn 12801 | . . . . . 6 | |
11 | 9, 10 | syl 14 | . . . . 5 |
12 | cntop1 12697 | . . . . 5 | |
13 | 11, 12 | syl 14 | . . . 4 |
14 | txhmeo.2 | . . . . 5 | |
15 | 14 | toptopon 12512 | . . . 4 TopOn |
16 | 13, 15 | sylib 121 | . . 3 TopOn |
17 | 8, 16 | cnmpt1st 12784 | . . . 4 |
18 | 8, 16, 17, 3 | cnmpt21f 12788 | . . 3 |
19 | 8, 16 | cnmpt2nd 12785 | . . . 4 |
20 | 8, 16, 19, 11 | cnmpt21f 12788 | . . 3 |
21 | 8, 16, 18, 20 | cnmpt2t 12789 | . 2 |
22 | vex 2715 | . . . . . . . . . . 11 | |
23 | vex 2715 | . . . . . . . . . . 11 | |
24 | 22, 23 | op1std 6099 | . . . . . . . . . 10 |
25 | 24 | fveq2d 5475 | . . . . . . . . 9 |
26 | 22, 23 | op2ndd 6100 | . . . . . . . . . 10 |
27 | 26 | fveq2d 5475 | . . . . . . . . 9 |
28 | 25, 27 | opeq12d 3751 | . . . . . . . 8 |
29 | 28 | mpompt 5916 | . . . . . . 7 |
30 | 29 | eqcomi 2161 | . . . . . 6 |
31 | eqid 2157 | . . . . . . . . . 10 | |
32 | 6, 31 | cnf 12700 | . . . . . . . . 9 |
33 | 3, 32 | syl 14 | . . . . . . . 8 |
34 | xp1st 6116 | . . . . . . . 8 | |
35 | ffvelrn 5603 | . . . . . . . 8 | |
36 | 33, 34, 35 | syl2an 287 | . . . . . . 7 |
37 | eqid 2157 | . . . . . . . . . 10 | |
38 | 14, 37 | cnf 12700 | . . . . . . . . 9 |
39 | 11, 38 | syl 14 | . . . . . . . 8 |
40 | xp2nd 6117 | . . . . . . . 8 | |
41 | ffvelrn 5603 | . . . . . . . 8 | |
42 | 39, 40, 41 | syl2an 287 | . . . . . . 7 |
43 | 36, 42 | opelxpd 4622 | . . . . . 6 |
44 | 6, 31 | hmeof1o 12805 | . . . . . . . . . 10 |
45 | 1, 44 | syl 14 | . . . . . . . . 9 |
46 | f1ocnv 5430 | . . . . . . . . 9 | |
47 | f1of 5417 | . . . . . . . . 9 | |
48 | 45, 46, 47 | 3syl 17 | . . . . . . . 8 |
49 | xp1st 6116 | . . . . . . . 8 | |
50 | ffvelrn 5603 | . . . . . . . 8 | |
51 | 48, 49, 50 | syl2an 287 | . . . . . . 7 |
52 | 14, 37 | hmeof1o 12805 | . . . . . . . . . 10 |
53 | 9, 52 | syl 14 | . . . . . . . . 9 |
54 | f1ocnv 5430 | . . . . . . . . 9 | |
55 | f1of 5417 | . . . . . . . . 9 | |
56 | 53, 54, 55 | 3syl 17 | . . . . . . . 8 |
57 | xp2nd 6117 | . . . . . . . 8 | |
58 | ffvelrn 5603 | . . . . . . . 8 | |
59 | 56, 57, 58 | syl2an 287 | . . . . . . 7 |
60 | 51, 59 | opelxpd 4622 | . . . . . 6 |
61 | 45 | adantr 274 | . . . . . . . . . 10 |
62 | 34 | ad2antrl 482 | . . . . . . . . . 10 |
63 | 49 | ad2antll 483 | . . . . . . . . . 10 |
64 | f1ocnvfvb 5733 | . . . . . . . . . 10 | |
65 | 61, 62, 63, 64 | syl3anc 1220 | . . . . . . . . 9 |
66 | eqcom 2159 | . . . . . . . . 9 | |
67 | eqcom 2159 | . . . . . . . . 9 | |
68 | 65, 66, 67 | 3bitr4g 222 | . . . . . . . 8 |
69 | 53 | adantr 274 | . . . . . . . . . 10 |
70 | 40 | ad2antrl 482 | . . . . . . . . . 10 |
71 | 57 | ad2antll 483 | . . . . . . . . . 10 |
72 | f1ocnvfvb 5733 | . . . . . . . . . 10 | |
73 | 69, 70, 71, 72 | syl3anc 1220 | . . . . . . . . 9 |
74 | eqcom 2159 | . . . . . . . . 9 | |
75 | eqcom 2159 | . . . . . . . . 9 | |
76 | 73, 74, 75 | 3bitr4g 222 | . . . . . . . 8 |
77 | 68, 76 | anbi12d 465 | . . . . . . 7 |
78 | eqop 6128 | . . . . . . . 8 | |
79 | 78 | ad2antll 483 | . . . . . . 7 |
80 | eqop 6128 | . . . . . . . 8 | |
81 | 80 | ad2antrl 482 | . . . . . . 7 |
82 | 77, 79, 81 | 3bitr4rd 220 | . . . . . 6 |
83 | 30, 43, 60, 82 | f1ocnv2d 6027 | . . . . 5 |
84 | 83 | simprd 113 | . . . 4 |
85 | vex 2715 | . . . . . . . 8 | |
86 | vex 2715 | . . . . . . . 8 | |
87 | 85, 86 | op1std 6099 | . . . . . . 7 |
88 | 87 | fveq2d 5475 | . . . . . 6 |
89 | 85, 86 | op2ndd 6100 | . . . . . . 7 |
90 | 89 | fveq2d 5475 | . . . . . 6 |
91 | 88, 90 | opeq12d 3751 | . . . . 5 |
92 | 91 | mpompt 5916 | . . . 4 |
93 | 84, 92 | eqtrdi 2206 | . . 3 |
94 | cntop2 12698 | . . . . . 6 | |
95 | 3, 94 | syl 14 | . . . . 5 |
96 | 31 | toptopon 12512 | . . . . 5 TopOn |
97 | 95, 96 | sylib 121 | . . . 4 TopOn |
98 | cntop2 12698 | . . . . . 6 | |
99 | 11, 98 | syl 14 | . . . . 5 |
100 | 37 | toptopon 12512 | . . . . 5 TopOn |
101 | 99, 100 | sylib 121 | . . . 4 TopOn |
102 | 97, 101 | cnmpt1st 12784 | . . . . 5 |
103 | hmeocnvcn 12802 | . . . . . 6 | |
104 | 1, 103 | syl 14 | . . . . 5 |
105 | 97, 101, 102, 104 | cnmpt21f 12788 | . . . 4 |
106 | 97, 101 | cnmpt2nd 12785 | . . . . 5 |
107 | hmeocnvcn 12802 | . . . . . 6 | |
108 | 9, 107 | syl 14 | . . . . 5 |
109 | 97, 101, 106, 108 | cnmpt21f 12788 | . . . 4 |
110 | 97, 101, 105, 109 | cnmpt2t 12789 | . . 3 |
111 | 93, 110 | eqeltrd 2234 | . 2 |
112 | ishmeo 12800 | . 2 | |
113 | 21, 111, 112 | sylanbrc 414 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wb 104 wceq 1335 wcel 2128 cop 3564 cuni 3774 cmpt 4028 cxp 4587 ccnv 4588 wf 5169 wf1o 5172 cfv 5173 (class class class)co 5827 cmpo 5829 c1st 6089 c2nd 6090 ctop 12491 TopOnctopon 12504 ccn 12681 ctx 12748 chmeo 12796 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-13 2130 ax-14 2131 ax-ext 2139 ax-coll 4082 ax-sep 4085 ax-pow 4138 ax-pr 4172 ax-un 4396 ax-setind 4499 |
This theorem depends on definitions: df-bi 116 df-3an 965 df-tru 1338 df-fal 1341 df-nf 1441 df-sb 1743 df-eu 2009 df-mo 2010 df-clab 2144 df-cleq 2150 df-clel 2153 df-nfc 2288 df-ne 2328 df-ral 2440 df-rex 2441 df-reu 2442 df-rab 2444 df-v 2714 df-sbc 2938 df-csb 3032 df-dif 3104 df-un 3106 df-in 3108 df-ss 3115 df-nul 3396 df-pw 3546 df-sn 3567 df-pr 3568 df-op 3570 df-uni 3775 df-iun 3853 df-br 3968 df-opab 4029 df-mpt 4030 df-id 4256 df-xp 4595 df-rel 4596 df-cnv 4597 df-co 4598 df-dm 4599 df-rn 4600 df-res 4601 df-ima 4602 df-iota 5138 df-fun 5175 df-fn 5176 df-f 5177 df-f1 5178 df-fo 5179 df-f1o 5180 df-fv 5181 df-ov 5830 df-oprab 5831 df-mpo 5832 df-1st 6091 df-2nd 6092 df-map 6598 df-topgen 12468 df-top 12492 df-topon 12505 df-bases 12537 df-cn 12684 df-tx 12749 df-hmeo 12797 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |