Theorem qtopcmp

Description: A quotient of a compact space is compact. (Contributed by Mario Carneiro, 24-Mar-2015)

	Ref	Expression
Hypothesis	qtopcmp.1	⊢ 𝑋 = ∪ 𝐽
Assertion	qtopcmp	⊢ ( ( 𝐽 ∈ Comp ∧ 𝐹 Fn 𝑋 ) → ( 𝐽 qTop 𝐹 ) ∈ Comp )

Proof

Step	Hyp	Ref	Expression
1		qtopcmp.1	⊢ 𝑋 = ∪ 𝐽
2		cmptop	⊢ ( 𝐽 ∈ Comp → 𝐽 ∈ Top )
3		eqid	⊢ ∪ ( 𝐽 qTop 𝐹 ) = ∪ ( 𝐽 qTop 𝐹 )
4	3	cncmp	⊢ ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ ∪ ( 𝐽 qTop 𝐹 ) ∧ 𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) ) → ( 𝐽 qTop 𝐹 ) ∈ Comp )
5	1 2 4	qtopcmplem	⊢ ( ( 𝐽 ∈ Comp ∧ 𝐹 Fn 𝑋 ) → ( 𝐽 qTop 𝐹 ) ∈ Comp )