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-1k∧∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡k
Assertion cvmshmeo ⊢T∈S⁡U∧A∈T→F↾A∈C↾𝑡AHomeoJ↾𝑡U

Proof

Step Hyp Ref Expression
1 cvmcov.1 ⊢S=k∈J⟼s∈𝒫C∖∅|⋃s=F-1k∧∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡k
2 1 cvmsi ⊢T∈S⁡U→U∈J∧T⊆C∧T≠∅∧⋃T=F-1U∧∀u∈T∀v∈T∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U
3 2 simp3d ⊢T∈S⁡U→⋃T=F-1U∧∀u∈T∀v∈T∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U
4 3 simprd ⊢T∈S⁡U→∀u∈T∀v∈T∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U
5 simpr ⊢∀v∈T∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U→F↾u∈C↾𝑡uHomeoJ↾𝑡U
6 5 ralimi ⊢∀u∈T∀v∈T∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U→∀u∈TF↾u∈C↾𝑡uHomeoJ↾𝑡U
7 4 6 syl ⊢T∈S⁡U→∀u∈TF↾u∈C↾𝑡uHomeoJ↾𝑡U
8 reseq2 ⊢u=A→F↾u=F↾A
9 oveq2 ⊢u=A→C↾𝑡u=C↾𝑡A
10 9 oveq1d ⊢u=A→C↾𝑡uHomeoJ↾𝑡U=C↾𝑡AHomeoJ↾𝑡U
11 8 10 eleq12d ⊢u=A→F↾u∈C↾𝑡uHomeoJ↾𝑡U↔F↾A∈C↾𝑡AHomeoJ↾𝑡U
12 11 rspccva ⊢∀u∈TF↾u∈C↾𝑡uHomeoJ↾𝑡U∧A∈T→F↾A∈C↾𝑡AHomeoJ↾𝑡U
13 7 12 sylan ⊢T∈S⁡U∧A∈T→F↾A∈C↾𝑡AHomeoJ↾𝑡U