Theorem cvmsrcl

Description: Reverse closure for an even covering. (Contributed by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Hypothesis	cvmcov.1	⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
Assertion	cvmsrcl	⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) → 𝑈 ∈ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		cvmcov.1	⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
2	1	dmmptss	⊢ dom 𝑆 ⊆ 𝐽
3		elfvdm	⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) → 𝑈 ∈ dom 𝑆 )
4	2 3	sseldi	⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) → 𝑈 ∈ 𝐽 )