Theorem cvmfo

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

	Ref	Expression
Hypotheses	cvmlift.1	⊢ 𝐵 = ∪ 𝐶
	cvmfo.2	⊢ 𝑋 = ∪ 𝐽
Assertion	cvmfo	⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐹 : 𝐵 –onto→ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		cvmlift.1	⊢ 𝐵 = ∪ 𝐶
2		cvmfo.2	⊢ 𝑋 = ∪ 𝐽
3		eqid	⊢ ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } ) = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
4	3	cvmscbv	⊢ ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } ) = ( 𝑎 ∈ 𝐽 ↦ { 𝑏 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑏 = ( ◡ 𝐹 “ 𝑎 ) ∧ ∀ 𝑐 ∈ 𝑏 ( ∀ 𝑑 ∈ ( 𝑏 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑎 ) ) ) ) } )
5	4 1 2	cvmfolem	⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐹 : 𝐵 –onto→ 𝑋 )