Metamath Proof Explorer


Theorem cvmsn0

Description: An even covering is nonempty. (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypothesis cvmcov.1 𝑆 = ( 𝑘𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( 𝑠 = ( 𝐹𝑘 ) ∧ ∀ 𝑢𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢𝑣 ) = ∅ ∧ ( 𝐹𝑢 ) ∈ ( ( 𝐶t 𝑢 ) Homeo ( 𝐽t 𝑘 ) ) ) ) } )
Assertion cvmsn0 ( 𝑇 ∈ ( 𝑆𝑈 ) → 𝑇 ≠ ∅ )

Proof

Step Hyp Ref Expression
1 cvmcov.1 𝑆 = ( 𝑘𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( 𝑠 = ( 𝐹𝑘 ) ∧ ∀ 𝑢𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢𝑣 ) = ∅ ∧ ( 𝐹𝑢 ) ∈ ( ( 𝐶t 𝑢 ) Homeo ( 𝐽t 𝑘 ) ) ) ) } )
2 1 cvmsi ( 𝑇 ∈ ( 𝑆𝑈 ) → ( 𝑈𝐽 ∧ ( 𝑇𝐶𝑇 ≠ ∅ ) ∧ ( 𝑇 = ( 𝐹𝑈 ) ∧ ∀ 𝑢𝑇 ( ∀ 𝑣 ∈ ( 𝑇 ∖ { 𝑢 } ) ( 𝑢𝑣 ) = ∅ ∧ ( 𝐹𝑢 ) ∈ ( ( 𝐶t 𝑢 ) Homeo ( 𝐽t 𝑈 ) ) ) ) ) )
3 2 simp2d ( 𝑇 ∈ ( 𝑆𝑈 ) → ( 𝑇𝐶𝑇 ≠ ∅ ) )
4 3 simprd ( 𝑇 ∈ ( 𝑆𝑈 ) → 𝑇 ≠ ∅ )