Metamath Proof Explorer


Theorem elqtop

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

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

Proof

Step Hyp Ref Expression
1 qtopval.1 𝑋 = 𝐽
2 1 qtopval2 ( ( 𝐽𝑉𝐹 : 𝑍onto𝑌𝑍𝑋 ) → ( 𝐽 qTop 𝐹 ) = { 𝑠 ∈ 𝒫 𝑌 ∣ ( 𝐹𝑠 ) ∈ 𝐽 } )
3 2 eleq2d ( ( 𝐽𝑉𝐹 : 𝑍onto𝑌𝑍𝑋 ) → ( 𝐴 ∈ ( 𝐽 qTop 𝐹 ) ↔ 𝐴 ∈ { 𝑠 ∈ 𝒫 𝑌 ∣ ( 𝐹𝑠 ) ∈ 𝐽 } ) )
4 imaeq2 ( 𝑠 = 𝐴 → ( 𝐹𝑠 ) = ( 𝐹𝐴 ) )
5 4 eleq1d ( 𝑠 = 𝐴 → ( ( 𝐹𝑠 ) ∈ 𝐽 ↔ ( 𝐹𝐴 ) ∈ 𝐽 ) )
6 5 elrab ( 𝐴 ∈ { 𝑠 ∈ 𝒫 𝑌 ∣ ( 𝐹𝑠 ) ∈ 𝐽 } ↔ ( 𝐴 ∈ 𝒫 𝑌 ∧ ( 𝐹𝐴 ) ∈ 𝐽 ) )
7 uniexg ( 𝐽𝑉 𝐽 ∈ V )
8 1 7 eqeltrid ( 𝐽𝑉𝑋 ∈ V )
9 8 3ad2ant1 ( ( 𝐽𝑉𝐹 : 𝑍onto𝑌𝑍𝑋 ) → 𝑋 ∈ V )
10 simp3 ( ( 𝐽𝑉𝐹 : 𝑍onto𝑌𝑍𝑋 ) → 𝑍𝑋 )
11 9 10 ssexd ( ( 𝐽𝑉𝐹 : 𝑍onto𝑌𝑍𝑋 ) → 𝑍 ∈ V )
12 simp2 ( ( 𝐽𝑉𝐹 : 𝑍onto𝑌𝑍𝑋 ) → 𝐹 : 𝑍onto𝑌 )
13 fornex ( 𝑍 ∈ V → ( 𝐹 : 𝑍onto𝑌𝑌 ∈ V ) )
14 11 12 13 sylc ( ( 𝐽𝑉𝐹 : 𝑍onto𝑌𝑍𝑋 ) → 𝑌 ∈ V )
15 elpw2g ( 𝑌 ∈ V → ( 𝐴 ∈ 𝒫 𝑌𝐴𝑌 ) )
16 14 15 syl ( ( 𝐽𝑉𝐹 : 𝑍onto𝑌𝑍𝑋 ) → ( 𝐴 ∈ 𝒫 𝑌𝐴𝑌 ) )
17 16 anbi1d ( ( 𝐽𝑉𝐹 : 𝑍onto𝑌𝑍𝑋 ) → ( ( 𝐴 ∈ 𝒫 𝑌 ∧ ( 𝐹𝐴 ) ∈ 𝐽 ) ↔ ( 𝐴𝑌 ∧ ( 𝐹𝐴 ) ∈ 𝐽 ) ) )
18 6 17 syl5bb ( ( 𝐽𝑉𝐹 : 𝑍onto𝑌𝑍𝑋 ) → ( 𝐴 ∈ { 𝑠 ∈ 𝒫 𝑌 ∣ ( 𝐹𝑠 ) ∈ 𝐽 } ↔ ( 𝐴𝑌 ∧ ( 𝐹𝐴 ) ∈ 𝐽 ) ) )
19 3 18 bitrd ( ( 𝐽𝑉𝐹 : 𝑍onto𝑌𝑍𝑋 ) → ( 𝐴 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝐴𝑌 ∧ ( 𝐹𝐴 ) ∈ 𝐽 ) ) )