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	⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
Assertion	cvmshmeo	⊢ ( ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ( 𝐹 ↾ 𝐴 ) ∈ ( ( 𝐶 ↾t 𝐴 ) Homeo ( 𝐽 ↾t 𝑈 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cvmcov.1	⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
2	1	cvmsi	⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) → ( 𝑈 ∈ 𝐽 ∧ ( 𝑇 ⊆ 𝐶 ∧ 𝑇 ≠ ∅ ) ∧ ( ∪ 𝑇 = ( ◡ 𝐹 “ 𝑈 ) ∧ ∀ 𝑢 ∈ 𝑇 ( ∀ 𝑣 ∈ ( 𝑇 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) ) ) )
3	2	simp3d	⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) → ( ∪ 𝑇 = ( ◡ 𝐹 “ 𝑈 ) ∧ ∀ 𝑢 ∈ 𝑇 ( ∀ 𝑣 ∈ ( 𝑇 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) ) )
4	3	simprd	⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) → ∀ 𝑢 ∈ 𝑇 ( ∀ 𝑣 ∈ ( 𝑇 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) )
5		simpr	⊢ ( ( ∀ 𝑣 ∈ ( 𝑇 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) → ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) )
6	5	ralimi	⊢ ( ∀ 𝑢 ∈ 𝑇 ( ∀ 𝑣 ∈ ( 𝑇 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) → ∀ 𝑢 ∈ 𝑇 ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) )
7	4 6	syl	⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) → ∀ 𝑢 ∈ 𝑇 ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) )
8		reseq2	⊢ ( 𝑢 = 𝐴 → ( 𝐹 ↾ 𝑢 ) = ( 𝐹 ↾ 𝐴 ) )
9		oveq2	⊢ ( 𝑢 = 𝐴 → ( 𝐶 ↾t 𝑢 ) = ( 𝐶 ↾t 𝐴 ) )
10	9	oveq1d	⊢ ( 𝑢 = 𝐴 → ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) = ( ( 𝐶 ↾t 𝐴 ) Homeo ( 𝐽 ↾t 𝑈 ) ) )
11	8 10	eleq12d	⊢ ( 𝑢 = 𝐴 → ( ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ↔ ( 𝐹 ↾ 𝐴 ) ∈ ( ( 𝐶 ↾t 𝐴 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) )
12	11	rspccva	⊢ ( ( ∀ 𝑢 ∈ 𝑇 ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ∧ 𝐴 ∈ 𝑇 ) → ( 𝐹 ↾ 𝐴 ) ∈ ( ( 𝐶 ↾t 𝐴 ) Homeo ( 𝐽 ↾t 𝑈 ) ) )
13	7 12	sylan	⊢ ( ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ( 𝐹 ↾ 𝐴 ) ∈ ( ( 𝐶 ↾t 𝐴 ) Homeo ( 𝐽 ↾t 𝑈 ) ) )