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 𝐹 ) ↔ ( 𝐴 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝐴 ) ∈ 𝐽 ) ) )