This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐹 ) ) )