Metamath Proof Explorer


Theorem elqtop3

Description: Value of the quotient topology function. (Contributed by Mario Carneiro, 9-Apr-2015)

Ref Expression
Assertion elqtop3 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋onto𝑌 ) → ( 𝐴 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝐴𝑌 ∧ ( 𝐹𝐴 ) ∈ 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 toponuni ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = 𝐽 )
2 eqimss ( 𝑋 = 𝐽𝑋 𝐽 )
3 1 2 syl ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 𝐽 )
4 3 adantr ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋onto𝑌 ) → 𝑋 𝐽 )
5 eqid 𝐽 = 𝐽
6 5 elqtop ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋onto𝑌𝑋 𝐽 ) → ( 𝐴 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝐴𝑌 ∧ ( 𝐹𝐴 ) ∈ 𝐽 ) ) )
7 4 6 mpd3an3 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋onto𝑌 ) → ( 𝐴 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝐴𝑌 ∧ ( 𝐹𝐴 ) ∈ 𝐽 ) ) )