Metamath Proof Explorer

Theorem cvmshmeo

Description: Every element of an even covering of U is homeomorphic to U via F . (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 cvmshmeo ⊢ T ∈ S ⁡ U ∧ A ∈ T → F ↾ A ∈ C ↾ 𝑡 A 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 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 simprd ⊢ T ∈ S ⁡ U → ∀ u ∈ T ∀ v ∈ T ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 U
5 simpr ⊢ ∀ v ∈ T ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 U → F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 U
6 5 ralimi ⊢ ∀ u ∈ T ∀ v ∈ T ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 U → ∀ u ∈ T F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 U
7 4 6 syl ⊢ T ∈ S ⁡ U → ∀ u ∈ T F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 U
8 reseq2 ⊢ u = A → F ↾ u = F ↾ A
9 oveq2 ⊢ u = A → C ↾ 𝑡 u = C ↾ 𝑡 A
10 9 oveq1d ⊢ u = A → C ↾ 𝑡 u Homeo J ↾ 𝑡 U = C ↾ 𝑡 A Homeo J ↾ 𝑡 U
11 8 10 eleq12d ⊢ u = A → F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 U ↔ F ↾ A ∈ C ↾ 𝑡 A Homeo J ↾ 𝑡 U
12 11 rspccva ⊢ ∀ u ∈ T F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 U ∧ A ∈ T → F ↾ A ∈ C ↾ 𝑡 A Homeo J ↾ 𝑡 U
13 7 12 sylan ⊢ T ∈ S ⁡ U ∧ A ∈ T → F ↾ A ∈ C ↾ 𝑡 A Homeo J ↾ 𝑡 U