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

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 focdmex ⊢ ( 𝑍 ∈ 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 bitrid ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( 𝐴 ∈ { 𝑠 ∈ 𝒫 𝑌 ∣ ( ◡ 𝐹 “ 𝑠 ) ∈ 𝐽 } ↔ ( 𝐴 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝐴 ) ∈ 𝐽 ) ) )
19 3 18 bitrd ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( 𝐴 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝐴 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝐴 ) ∈ 𝐽 ) ) )