Metamath Proof Explorer


Theorem cvmcn

Description: A covering map is a continuous function. (Contributed by Mario Carneiro, 13-Feb-2015)

Ref Expression
Assertion cvmcn ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐹 ∈ ( 𝐶 Cn 𝐽 ) )

Proof

Step Hyp Ref Expression
1 eqid ( 𝑘𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( 𝑠 = ( 𝐹𝑘 ) ∧ ∀ 𝑢𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢𝑣 ) = ∅ ∧ ( 𝐹𝑢 ) ∈ ( ( 𝐶t 𝑢 ) Homeo ( 𝐽t 𝑘 ) ) ) ) } ) = ( 𝑘𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( 𝑠 = ( 𝐹𝑘 ) ∧ ∀ 𝑢𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢𝑣 ) = ∅ ∧ ( 𝐹𝑢 ) ∈ ( ( 𝐶t 𝑢 ) Homeo ( 𝐽t 𝑘 ) ) ) ) } )
2 eqid 𝐽 = 𝐽
3 1 2 iscvm ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ↔ ( ( 𝐶 ∈ Top ∧ 𝐽 ∈ Top ∧ 𝐹 ∈ ( 𝐶 Cn 𝐽 ) ) ∧ ∀ 𝑥 𝐽𝑘𝐽 ( 𝑥𝑘 ∧ ( ( 𝑘𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( 𝑠 = ( 𝐹𝑘 ) ∧ ∀ 𝑢𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢𝑣 ) = ∅ ∧ ( 𝐹𝑢 ) ∈ ( ( 𝐶t 𝑢 ) Homeo ( 𝐽t 𝑘 ) ) ) ) } ) ‘ 𝑘 ) ≠ ∅ ) ) )
4 3 simplbi ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → ( 𝐶 ∈ Top ∧ 𝐽 ∈ Top ∧ 𝐹 ∈ ( 𝐶 Cn 𝐽 ) ) )
5 4 simp3d ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐹 ∈ ( 𝐶 Cn 𝐽 ) )