Theorem qtopid

Description: A quotient map is a continuous function into its quotient topology. (Contributed by Mario Carneiro, 23-Mar-2015)

	Ref	Expression
Assertion	qtopid	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 Fn 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 Fn 𝑋 ) → 𝐹 Fn 𝑋 )
2		dffn4	⊢ ( 𝐹 Fn 𝑋 ↔ 𝐹 : 𝑋 –onto→ ran 𝐹 )
3	1 2	sylib	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 Fn 𝑋 ) → 𝐹 : 𝑋 –onto→ ran 𝐹 )
4		fof	⊢ ( 𝐹 : 𝑋 –onto→ ran 𝐹 → 𝐹 : 𝑋 ⟶ ran 𝐹 )
5	3 4	syl	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 Fn 𝑋 ) → 𝐹 : 𝑋 ⟶ ran 𝐹 )
6		elqtop3	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ ran 𝐹 ) → ( 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝑥 ⊆ ran 𝐹 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) )
7	3 6	syldan	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 Fn 𝑋 ) → ( 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝑥 ⊆ ran 𝐹 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) )
8	7	simplbda	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 Fn 𝑋 ) ∧ 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ) → ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 )
9	8	ralrimiva	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 Fn 𝑋 ) → ∀ 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 )
10		qtoptopon	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ ran 𝐹 ) → ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ ran 𝐹 ) )
11	3 10	syldan	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 Fn 𝑋 ) → ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ ran 𝐹 ) )
12		iscn	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ ran 𝐹 ) ) → ( 𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) ↔ ( 𝐹 : 𝑋 ⟶ ran 𝐹 ∧ ∀ 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) )
13	11 12	syldan	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 Fn 𝑋 ) → ( 𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) ↔ ( 𝐹 : 𝑋 ⟶ ran 𝐹 ∧ ∀ 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) )
14	5 9 13	mpbir2and	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 Fn 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) )