Metamath Proof Explorer


Theorem cvmsval

Description: Elementhood in the set S of all even coverings of an open set in J . S is an even covering of U if it is a nonempty collection of disjoint open sets in C whose union is the preimage of U , such that each set u e. S is homeomorphic under F to U . (Contributed by Mario Carneiro, 13-Feb-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 cvmsval C V T S U U J T C T T = F -1 U u T v T u u v = F u C 𝑡 u Homeo J 𝑡 U

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 1 cvmsi T S U U J T C T T = F -1 U u T v T u u v = F u C 𝑡 u Homeo J 𝑡 U
3 3anass U J T C T T = F -1 U u T v T u u v = F u C 𝑡 u Homeo J 𝑡 U U J T C T T = F -1 U u T v T u u v = F u C 𝑡 u Homeo J 𝑡 U
4 id U J U J
5 pwexg C V 𝒫 C V
6 difexg 𝒫 C V 𝒫 C V
7 rabexg 𝒫 C V s 𝒫 C | s = F -1 U u s v s u u v = F u C 𝑡 u Homeo J 𝑡 U V
8 5 6 7 3syl C V s 𝒫 C | s = F -1 U u s v s u u v = F u C 𝑡 u Homeo J 𝑡 U V
9 imaeq2 k = U F -1 k = F -1 U
10 9 eqeq2d k = U s = F -1 k s = F -1 U
11 oveq2 k = U J 𝑡 k = J 𝑡 U
12 11 oveq2d k = U C 𝑡 u Homeo J 𝑡 k = C 𝑡 u Homeo J 𝑡 U
13 12 eleq2d k = U F u C 𝑡 u Homeo J 𝑡 k F u C 𝑡 u Homeo J 𝑡 U
14 13 anbi2d k = U v s u u v = F u C 𝑡 u Homeo J 𝑡 k v s u u v = F u C 𝑡 u Homeo J 𝑡 U
15 14 ralbidv k = U u s v s u u v = F u C 𝑡 u Homeo J 𝑡 k u s v s u u v = F u C 𝑡 u Homeo J 𝑡 U
16 10 15 anbi12d k = U s = F -1 k u s v s u u v = F u C 𝑡 u Homeo J 𝑡 k s = F -1 U u s v s u u v = F u C 𝑡 u Homeo J 𝑡 U
17 16 rabbidv k = U s 𝒫 C | s = F -1 k u s v s u u v = F u C 𝑡 u Homeo J 𝑡 k = s 𝒫 C | s = F -1 U u s v s u u v = F u C 𝑡 u Homeo J 𝑡 U
18 17 1 fvmptg U J s 𝒫 C | s = F -1 U u s v s u u v = F u C 𝑡 u Homeo J 𝑡 U V S U = s 𝒫 C | s = F -1 U u s v s u u v = F u C 𝑡 u Homeo J 𝑡 U
19 4 8 18 syl2anr C V U J S U = s 𝒫 C | s = F -1 U u s v s u u v = F u C 𝑡 u Homeo J 𝑡 U
20 19 eleq2d C V U J T S U T s 𝒫 C | s = F -1 U u s v s u u v = F u C 𝑡 u Homeo J 𝑡 U
21 unieq s = T s = T
22 21 eqeq1d s = T s = F -1 U T = F -1 U
23 difeq1 s = T s u = T u
24 23 raleqdv s = T v s u u v = v T u u v =
25 24 anbi1d s = T v s u u v = F u C 𝑡 u Homeo J 𝑡 U v T u u v = F u C 𝑡 u Homeo J 𝑡 U
26 25 raleqbi1dv s = T u s v s u u v = F u C 𝑡 u Homeo J 𝑡 U u T v T u u v = F u C 𝑡 u Homeo J 𝑡 U
27 22 26 anbi12d s = T s = F -1 U u s v s u u v = F u C 𝑡 u Homeo J 𝑡 U T = F -1 U u T v T u u v = F u C 𝑡 u Homeo J 𝑡 U
28 27 elrab T s 𝒫 C | s = F -1 U u s v s u u v = F u C 𝑡 u Homeo J 𝑡 U T 𝒫 C T = F -1 U u T v T u u v = F u C 𝑡 u Homeo J 𝑡 U
29 eldifsn T 𝒫 C T 𝒫 C T
30 elpw2g C V T 𝒫 C T C
31 30 adantr C V U J T 𝒫 C T C
32 31 anbi1d C V U J T 𝒫 C T T C T
33 29 32 syl5bb C V U J T 𝒫 C T C T
34 33 anbi1d C V U J T 𝒫 C T = F -1 U u T v T u u v = F u C 𝑡 u Homeo J 𝑡 U T C T T = F -1 U u T v T u u v = F u C 𝑡 u Homeo J 𝑡 U
35 28 34 syl5bb C V U J T s 𝒫 C | s = F -1 U u s v s u u v = F u C 𝑡 u Homeo J 𝑡 U T C T T = F -1 U u T v T u u v = F u C 𝑡 u Homeo J 𝑡 U
36 20 35 bitrd C V U J T S U T C T T = F -1 U u T v T u u v = F u C 𝑡 u Homeo J 𝑡 U
37 36 biimprd C V U J T C T T = F -1 U u T v T u u v = F u C 𝑡 u Homeo J 𝑡 U T S U
38 37 expimpd C V U J T C T T = F -1 U u T v T u u v = F u C 𝑡 u Homeo J 𝑡 U T S U
39 3 38 syl5bi C V U J T C T T = F -1 U u T v T u u v = F u C 𝑡 u Homeo J 𝑡 U T S U
40 2 39 impbid2 C V T S U U J T C T T = F -1 U u T v T u u v = F u C 𝑡 u Homeo J 𝑡 U