Metamath Proof Explorer


Theorem cvmsss2

Description: An open subset of an evenly covered set is evenly covered. (Contributed by Mario Carneiro, 7-Jul-2015)

Ref Expression
Hypothesis cvmcov.1 S = k J s 𝒫 C | s = F -1 k u s v s u u v = F u C 𝑡 u Homeo J 𝑡 k
Assertion cvmsss2 F C CovMap J V J V U S U S V

Proof

Step Hyp Ref Expression
1 cvmcov.1 S = k J s 𝒫 C | s = F -1 k u s v s u u v = F u C 𝑡 u Homeo J 𝑡 k
2 n0 S U x x S U
3 simpl2 F C CovMap J V J V U x S U V J
4 simpl1 F C CovMap J V J V U x S U F C CovMap J
5 cvmtop1 F C CovMap J C Top
6 4 5 syl F C CovMap J V J V U x S U C Top
7 6 adantr F C CovMap J V J V U x S U y x C Top
8 1 cvmsss x S U x C
9 8 adantl F C CovMap J V J V U x S U x C
10 9 sselda F C CovMap J V J V U x S U y x y C
11 cvmcn F C CovMap J F C Cn J
12 4 11 syl F C CovMap J V J V U x S U F C Cn J
13 cnima F C Cn J V J F -1 V C
14 12 3 13 syl2anc F C CovMap J V J V U x S U F -1 V C
15 14 adantr F C CovMap J V J V U x S U y x F -1 V C
16 inopn C Top y C F -1 V C y F -1 V C
17 7 10 15 16 syl3anc F C CovMap J V J V U x S U y x y F -1 V C
18 17 fmpttd F C CovMap J V J V U x S U y x y F -1 V : x C
19 18 frnd F C CovMap J V J V U x S U ran y x y F -1 V C
20 1 cvmsn0 x S U x
21 20 adantl F C CovMap J V J V U x S U x
22 dmmptg y x y F -1 V V dom y x y F -1 V = x
23 inex1g y x y F -1 V V
24 22 23 mprg dom y x y F -1 V = x
25 24 eqeq1i dom y x y F -1 V = x =
26 dm0rn0 dom y x y F -1 V = ran y x y F -1 V =
27 25 26 bitr3i x = ran y x y F -1 V =
28 27 necon3bii x ran y x y F -1 V
29 21 28 sylib F C CovMap J V J V U x S U ran y x y F -1 V
30 19 29 jca F C CovMap J V J V U x S U ran y x y F -1 V C ran y x y F -1 V
31 inss2 y F -1 V F -1 V
32 elpw2g F -1 V C y F -1 V 𝒫 F -1 V y F -1 V F -1 V
33 15 32 syl F C CovMap J V J V U x S U y x y F -1 V 𝒫 F -1 V y F -1 V F -1 V
34 31 33 mpbiri F C CovMap J V J V U x S U y x y F -1 V 𝒫 F -1 V
35 34 fmpttd F C CovMap J V J V U x S U y x y F -1 V : x 𝒫 F -1 V
36 35 frnd F C CovMap J V J V U x S U ran y x y F -1 V 𝒫 F -1 V
37 sspwuni ran y x y F -1 V 𝒫 F -1 V ran y x y F -1 V F -1 V
38 36 37 sylib F C CovMap J V J V U x S U ran y x y F -1 V F -1 V
39 simpl3 F C CovMap J V J V U x S U V U
40 imass2 V U F -1 V F -1 U
41 39 40 syl F C CovMap J V J V U x S U F -1 V F -1 U
42 1 cvmsuni x S U x = F -1 U
43 42 adantl F C CovMap J V J V U x S U x = F -1 U
44 41 43 sseqtrrd F C CovMap J V J V U x S U F -1 V x
45 44 sselda F C CovMap J V J V U x S U z F -1 V z x
46 eqid t F -1 V = t F -1 V
47 ineq1 y = t y F -1 V = t F -1 V
48 47 rspceeqv t x t F -1 V = t F -1 V y x t F -1 V = y F -1 V
49 46 48 mpan2 t x y x t F -1 V = y F -1 V
50 49 ad2antrl F C CovMap J V J V U x S U z F -1 V t x z t y x t F -1 V = y F -1 V
51 vex t V
52 51 inex1 t F -1 V V
53 eqid y x y F -1 V = y x y F -1 V
54 53 elrnmpt t F -1 V V t F -1 V ran y x y F -1 V y x t F -1 V = y F -1 V
55 52 54 ax-mp t F -1 V ran y x y F -1 V y x t F -1 V = y F -1 V
56 50 55 sylibr F C CovMap J V J V U x S U z F -1 V t x z t t F -1 V ran y x y F -1 V
57 simprr F C CovMap J V J V U x S U z F -1 V t x z t z t
58 simplr F C CovMap J V J V U x S U z F -1 V t x z t z F -1 V
59 57 58 elind F C CovMap J V J V U x S U z F -1 V t x z t z t F -1 V
60 eleq2 w = t F -1 V z w z t F -1 V
61 60 rspcev t F -1 V ran y x y F -1 V z t F -1 V w ran y x y F -1 V z w
62 56 59 61 syl2anc F C CovMap J V J V U x S U z F -1 V t x z t w ran y x y F -1 V z w
63 62 rexlimdvaa F C CovMap J V J V U x S U z F -1 V t x z t w ran y x y F -1 V z w
64 eluni2 z x t x z t
65 eluni2 z ran y x y F -1 V w ran y x y F -1 V z w
66 63 64 65 3imtr4g F C CovMap J V J V U x S U z F -1 V z x z ran y x y F -1 V
67 45 66 mpd F C CovMap J V J V U x S U z F -1 V z ran y x y F -1 V
68 38 67 eqelssd F C CovMap J V J V U x S U ran y x y F -1 V = F -1 V
69 eldifsn z ran y x y F -1 V t F -1 V z ran y x y F -1 V z t F -1 V
70 vex z V
71 53 elrnmpt z V z ran y x y F -1 V y x z = y F -1 V
72 70 71 ax-mp z ran y x y F -1 V y x z = y F -1 V
73 47 equcoms t = y y F -1 V = t F -1 V
74 73 necon3ai y F -1 V t F -1 V ¬ t = y
75 simpllr F C CovMap J V J V U x S U t x y x x S U
76 simplr F C CovMap J V J V U x S U t x y x t x
77 simpr F C CovMap J V J V U x S U t x y x y x
78 1 cvmsdisj x S U t x y x t = y t y =
79 75 76 77 78 syl3anc F C CovMap J V J V U x S U t x y x t = y t y =
80 79 ord F C CovMap J V J V U x S U t x y x ¬ t = y t y =
81 inss1 t y F -1 V t y
82 sseq0 t y F -1 V t y t y = t y F -1 V =
83 81 82 mpan t y = t y F -1 V =
84 74 80 83 syl56 F C CovMap J V J V U x S U t x y x y F -1 V t F -1 V t y F -1 V =
85 neeq1 z = y F -1 V z t F -1 V y F -1 V t F -1 V
86 ineq2 z = y F -1 V t F -1 V z = t F -1 V y F -1 V
87 inindir t y F -1 V = t F -1 V y F -1 V
88 86 87 eqtr4di z = y F -1 V t F -1 V z = t y F -1 V
89 88 eqeq1d z = y F -1 V t F -1 V z = t y F -1 V =
90 85 89 imbi12d z = y F -1 V z t F -1 V t F -1 V z = y F -1 V t F -1 V t y F -1 V =
91 84 90 syl5ibrcom F C CovMap J V J V U x S U t x y x z = y F -1 V z t F -1 V t F -1 V z =
92 91 rexlimdva F C CovMap J V J V U x S U t x y x z = y F -1 V z t F -1 V t F -1 V z =
93 72 92 syl5bi F C CovMap J V J V U x S U t x z ran y x y F -1 V z t F -1 V t F -1 V z =
94 93 impd F C CovMap J V J V U x S U t x z ran y x y F -1 V z t F -1 V t F -1 V z =
95 69 94 syl5bi F C CovMap J V J V U x S U t x z ran y x y F -1 V t F -1 V t F -1 V z =
96 95 ralrimiv F C CovMap J V J V U x S U t x z ran y x y F -1 V t F -1 V t F -1 V z =
97 inss1 t F -1 V t
98 resabs1 t F -1 V t F t t F -1 V = F t F -1 V
99 97 98 ax-mp F t t F -1 V = F t F -1 V
100 1 cvmshmeo x S U t x F t C 𝑡 t Homeo J 𝑡 U
101 100 adantll F C CovMap J V J V U x S U t x F t C 𝑡 t Homeo J 𝑡 U
102 6 adantr F C CovMap J V J V U x S U t x C Top
103 9 sselda F C CovMap J V J V U x S U t x t C
104 elssuni t C t C
105 103 104 syl F C CovMap J V J V U x S U t x t C
106 eqid C = C
107 106 restuni C Top t C t = C 𝑡 t
108 102 105 107 syl2anc F C CovMap J V J V U x S U t x t = C 𝑡 t
109 97 108 sseqtrid F C CovMap J V J V U x S U t x t F -1 V C 𝑡 t
110 eqid C 𝑡 t = C 𝑡 t
111 110 hmeores F t C 𝑡 t Homeo J 𝑡 U t F -1 V C 𝑡 t F t t F -1 V C 𝑡 t 𝑡 t F -1 V Homeo J 𝑡 U 𝑡 F t t F -1 V
112 101 109 111 syl2anc F C CovMap J V J V U x S U t x F t t F -1 V C 𝑡 t 𝑡 t F -1 V Homeo J 𝑡 U 𝑡 F t t F -1 V
113 99 112 eqeltrrid F C CovMap J V J V U x S U t x F t F -1 V C 𝑡 t 𝑡 t F -1 V Homeo J 𝑡 U 𝑡 F t t F -1 V
114 97 a1i F C CovMap J V J V U x S U t x t F -1 V t
115 simpr F C CovMap J V J V U x S U t x t x
116 restabs C Top t F -1 V t t x C 𝑡 t 𝑡 t F -1 V = C 𝑡 t F -1 V
117 102 114 115 116 syl3anc F C CovMap J V J V U x S U t x C 𝑡 t 𝑡 t F -1 V = C 𝑡 t F -1 V
118 incom t F -1 V = F -1 V t
119 cnvresima F t -1 V = F -1 V t
120 118 119 eqtr4i t F -1 V = F t -1 V
121 120 imaeq2i F t t F -1 V = F t F t -1 V
122 4 adantr F C CovMap J V J V U x S U t x F C CovMap J
123 simplr F C CovMap J V J V U x S U t x x S U
124 1 cvmsf1o F C CovMap J x S U t x F t : t 1-1 onto U
125 122 123 115 124 syl3anc F C CovMap J V J V U x S U t x F t : t 1-1 onto U
126 f1ofo F t : t 1-1 onto U F t : t onto U
127 125 126 syl F C CovMap J V J V U x S U t x F t : t onto U
128 39 adantr F C CovMap J V J V U x S U t x V U
129 foimacnv F t : t onto U V U F t F t -1 V = V
130 127 128 129 syl2anc F C CovMap J V J V U x S U t x F t F t -1 V = V
131 121 130 syl5eq F C CovMap J V J V U x S U t x F t t F -1 V = V
132 131 oveq2d F C CovMap J V J V U x S U t x J 𝑡 U 𝑡 F t t F -1 V = J 𝑡 U 𝑡 V
133 cvmtop2 F C CovMap J J Top
134 4 133 syl F C CovMap J V J V U x S U J Top
135 1 cvmsrcl x S U U J
136 135 adantl F C CovMap J V J V U x S U U J
137 restabs J Top V U U J J 𝑡 U 𝑡 V = J 𝑡 V
138 134 39 136 137 syl3anc F C CovMap J V J V U x S U J 𝑡 U 𝑡 V = J 𝑡 V
139 138 adantr F C CovMap J V J V U x S U t x J 𝑡 U 𝑡 V = J 𝑡 V
140 132 139 eqtrd F C CovMap J V J V U x S U t x J 𝑡 U 𝑡 F t t F -1 V = J 𝑡 V
141 117 140 oveq12d F C CovMap J V J V U x S U t x C 𝑡 t 𝑡 t F -1 V Homeo J 𝑡 U 𝑡 F t t F -1 V = C 𝑡 t F -1 V Homeo J 𝑡 V
142 113 141 eleqtrd F C CovMap J V J V U x S U t x F t F -1 V C 𝑡 t F -1 V Homeo J 𝑡 V
143 96 142 jca F C CovMap J V J V U x S U t x z ran y x y F -1 V t F -1 V t F -1 V z = F t F -1 V C 𝑡 t F -1 V Homeo J 𝑡 V
144 143 ralrimiva F C CovMap J V J V U x S U t x z ran y x y F -1 V t F -1 V t F -1 V z = F t F -1 V C 𝑡 t F -1 V Homeo J 𝑡 V
145 52 rgenw t x t F -1 V V
146 47 cbvmptv y x y F -1 V = t x t F -1 V
147 sneq w = t F -1 V w = t F -1 V
148 147 difeq2d w = t F -1 V ran y x y F -1 V w = ran y x y F -1 V t F -1 V
149 ineq1 w = t F -1 V w z = t F -1 V z
150 149 eqeq1d w = t F -1 V w z = t F -1 V z =
151 148 150 raleqbidv w = t F -1 V z ran y x y F -1 V w w z = z ran y x y F -1 V t F -1 V t F -1 V z =
152 reseq2 w = t F -1 V F w = F t F -1 V
153 oveq2 w = t F -1 V C 𝑡 w = C 𝑡 t F -1 V
154 153 oveq1d w = t F -1 V C 𝑡 w Homeo J 𝑡 V = C 𝑡 t F -1 V Homeo J 𝑡 V
155 152 154 eleq12d w = t F -1 V F w C 𝑡 w Homeo J 𝑡 V F t F -1 V C 𝑡 t F -1 V Homeo J 𝑡 V
156 151 155 anbi12d w = t F -1 V z ran y x y F -1 V w w z = F w C 𝑡 w Homeo J 𝑡 V z ran y x y F -1 V t F -1 V t F -1 V z = F t F -1 V C 𝑡 t F -1 V Homeo J 𝑡 V
157 146 156 ralrnmptw t x t F -1 V V w ran y x y F -1 V z ran y x y F -1 V w w z = F w C 𝑡 w Homeo J 𝑡 V t x z ran y x y F -1 V t F -1 V t F -1 V z = F t F -1 V C 𝑡 t F -1 V Homeo J 𝑡 V
158 145 157 ax-mp w ran y x y F -1 V z ran y x y F -1 V w w z = F w C 𝑡 w Homeo J 𝑡 V t x z ran y x y F -1 V t F -1 V t F -1 V z = F t F -1 V C 𝑡 t F -1 V Homeo J 𝑡 V
159 144 158 sylibr F C CovMap J V J V U x S U w ran y x y F -1 V z ran y x y F -1 V w w z = F w C 𝑡 w Homeo J 𝑡 V
160 68 159 jca F C CovMap J V J V U x S U ran y x y F -1 V = F -1 V w ran y x y F -1 V z ran y x y F -1 V w w z = F w C 𝑡 w Homeo J 𝑡 V
161 1 cvmscbv S = a J b 𝒫 C | b = F -1 a w b z b w w z = F w C 𝑡 w Homeo J 𝑡 a
162 161 cvmsval C Top ran y x y F -1 V S V V J ran y x y F -1 V C ran y x y F -1 V ran y x y F -1 V = F -1 V w ran y x y F -1 V z ran y x y F -1 V w w z = F w C 𝑡 w Homeo J 𝑡 V
163 6 162 syl F C CovMap J V J V U x S U ran y x y F -1 V S V V J ran y x y F -1 V C ran y x y F -1 V ran y x y F -1 V = F -1 V w ran y x y F -1 V z ran y x y F -1 V w w z = F w C 𝑡 w Homeo J 𝑡 V
164 3 30 160 163 mpbir3and F C CovMap J V J V U x S U ran y x y F -1 V S V
165 164 ne0d F C CovMap J V J V U x S U S V
166 165 ex F C CovMap J V J V U x S U S V
167 166 exlimdv F C CovMap J V J V U x x S U S V
168 2 167 syl5bi F C CovMap J V J V U S U S V