Metamath Proof Explorer

Theorem cvmsi

Description: One direction of cvmsval . (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 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

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 cvmsrcl ⊢ T ∈ S ⁡ U → U ∈ J
3 imaeq2 ⊢ k = U → F -1 k = F -1 U
4 3 eqeq2d ⊢ k = U → ⋃ s = F -1 k ↔ ⋃ s = F -1 U
5 oveq2 ⊢ k = U → J ↾ 𝑡 k = J ↾ 𝑡 U
6 5 oveq2d ⊢ k = U → C ↾ 𝑡 u Homeo J ↾ 𝑡 k = C ↾ 𝑡 u Homeo J ↾ 𝑡 U
7 6 eleq2d ⊢ k = U → F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 k ↔ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 U
8 7 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
9 8 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
10 4 9 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
11 10 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
12 11 1 fvmptss2 ⊢ S ⁡ U ⊆ s ∈ 𝒫 C ∖ ∅ | ⋃ s = F -1 U ∧ ∀ u ∈ s ∀ v ∈ s ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 U
13 12 sseli ⊢ T ∈ S ⁡ U → T ∈ s ∈ 𝒫 C ∖ ∅ | ⋃ s = F -1 U ∧ ∀ u ∈ s ∀ v ∈ s ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 U
14 unieq ⊢ s = T → ⋃ s = ⋃ T
15 14 eqeq1d ⊢ s = T → ⋃ s = F -1 U ↔ ⋃ T = F -1 U
16 difeq1 ⊢ s = T → s ∖ u = T ∖ u
17 16 raleqdv ⊢ s = T → ∀ v ∈ s ∖ u u ∩ v = ∅ ↔ ∀ v ∈ T ∖ u u ∩ v = ∅
18 17 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
19 18 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
20 15 19 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
21 20 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
22 13 21 sylib ⊢ T ∈ S ⁡ U → T ∈ 𝒫 C ∖ ∅ ∧ ⋃ T = F -1 U ∧ ∀ u ∈ T ∀ v ∈ T ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 U
23 22 simpld ⊢ T ∈ S ⁡ U → T ∈ 𝒫 C ∖ ∅
24 eldifsn ⊢ T ∈ 𝒫 C ∖ ∅ ↔ T ∈ 𝒫 C ∧ T ≠ ∅
25 23 24 sylib ⊢ T ∈ S ⁡ U → T ∈ 𝒫 C ∧ T ≠ ∅
26 elpwi ⊢ T ∈ 𝒫 C → T ⊆ C
27 26 anim1i ⊢ T ∈ 𝒫 C ∧ T ≠ ∅ → T ⊆ C ∧ T ≠ ∅
28 25 27 syl ⊢ T ∈ S ⁡ U → T ⊆ C ∧ T ≠ ∅
29 22 simprd ⊢ T ∈ S ⁡ U → ⋃ T = F -1 U ∧ ∀ u ∈ T ∀ v ∈ T ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 U
30 2 28 29 3jca ⊢ 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