Metamath Proof Explorer


Theorem elqtop2

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

Ref Expression
Hypothesis qtoptop.1 𝑋 = 𝐽
Assertion elqtop2 ( ( 𝐽𝑉𝐹 : 𝑋onto𝑌 ) → ( 𝐴 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝐴𝑌 ∧ ( 𝐹𝐴 ) ∈ 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 qtoptop.1 𝑋 = 𝐽
2 ssid 𝑋𝑋
3 1 elqtop ( ( 𝐽𝑉𝐹 : 𝑋onto𝑌𝑋𝑋 ) → ( 𝐴 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝐴𝑌 ∧ ( 𝐹𝐴 ) ∈ 𝐽 ) ) )
4 2 3 mp3an3 ( ( 𝐽𝑉𝐹 : 𝑋onto𝑌 ) → ( 𝐴 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝐴𝑌 ∧ ( 𝐹𝐴 ) ∈ 𝐽 ) ) )