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		dffn4	⊢ ( 𝐹 Fn 𝑋 ↔ 𝐹 : 𝑋 –onto→ ran 𝐹 )
2	1	bilani	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 Fn 𝑋 ) → 𝐹 : 𝑋 –onto→ ran 𝐹 )
3		fof	⊢ ( 𝐹 : 𝑋 –onto→ ran 𝐹 → 𝐹 : 𝑋 ⟶ ran 𝐹 )
4	2 3	syl	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 Fn 𝑋 ) → 𝐹 : 𝑋 ⟶ ran 𝐹 )
5		elqtop3	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ ran 𝐹 ) → ( 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝑥 ⊆ ran 𝐹 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) )
6	2 5	syldan	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 Fn 𝑋 ) → ( 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝑥 ⊆ ran 𝐹 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) )
7	6	simplbda	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 Fn 𝑋 ) ∧ 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ) → ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 )
8	7	ralrimiva	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 Fn 𝑋 ) → ∀ 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 )
9		qtoptopon	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ ran 𝐹 ) → ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ ran 𝐹 ) )
10	2 9	syldan	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 Fn 𝑋 ) → ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ ran 𝐹 ) )
11		iscn	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ ran 𝐹 ) ) → ( 𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) ↔ ( 𝐹 : 𝑋 ⟶ ran 𝐹 ∧ ∀ 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) )
12	10 11	syldan	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 Fn 𝑋 ) → ( 𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) ↔ ( 𝐹 : 𝑋 ⟶ ran 𝐹 ∧ ∀ 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) )
13	4 8 12	mpbir2and	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 Fn 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) )