Metamath Proof Explorer

Theorem cvmsuni

Description: An even covering of U has union equal to the preimage of U by F . (Contributed by Mario Carneiro, 11-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 cvmsuni ⊢ T ∈ S ⁡ U → ⋃ T = F -1 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 2 simp3d ⊢ T ∈ S ⁡ U → ⋃ T = F -1 U ∧ ∀ u ∈ T ∀ v ∈ T ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 U
4 3 simpld ⊢ T ∈ S ⁡ U → ⋃ T = F -1 U