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