Metamath Proof Explorer

Theorem qtopval2

Description: Value of the quotient topology function when F is a function on the base set. (Contributed by Mario Carneiro, 23-Mar-2015)

Ref Expression
Hypothesis qtopval.1 ⊢ 𝑋 = ∪ 𝐽
Assertion qtopval2 ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( 𝐽 qTop 𝐹 ) = { 𝑠 ∈ 𝒫 𝑌 ∣ ( ◡ 𝐹 “ 𝑠 ) ∈ 𝐽 } )

Proof

Step Hyp Ref Expression
1 qtopval.1 ⊢ 𝑋 = ∪ 𝐽
2 simp1 ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → 𝐽 ∈ 𝑉 )
3 fof ⊢ ( 𝐹 : 𝑍 –onto→ 𝑌 → 𝐹 : 𝑍 ⟶ 𝑌 )
4 3 3ad2ant2 ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → 𝐹 : 𝑍 ⟶ 𝑌 )
5 uniexg ⊢ ( 𝐽 ∈ 𝑉 → ∪ 𝐽 ∈ V )
6 5 3ad2ant1 ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ∪ 𝐽 ∈ V )
7 1 6 eqeltrid ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → 𝑋 ∈ V )
8 simp3 ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → 𝑍 ⊆ 𝑋 )
9 7 8 ssexd ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → 𝑍 ∈ V )
10 fex ⊢ ( ( 𝐹 : 𝑍 ⟶ 𝑌 ∧ 𝑍 ∈ V ) → 𝐹 ∈ V )
11 4 9 10 syl2anc ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → 𝐹 ∈ V )
12 1 qtopval ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 ∈ V ) → ( 𝐽 qTop 𝐹 ) = { 𝑠 ∈ 𝒫 ( 𝐹 “ 𝑋 ) ∣ ( ( ◡ 𝐹 “ 𝑠 ) ∩ 𝑋 ) ∈ 𝐽 } )
13 2 11 12 syl2anc ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( 𝐽 qTop 𝐹 ) = { 𝑠 ∈ 𝒫 ( 𝐹 “ 𝑋 ) ∣ ( ( ◡ 𝐹 “ 𝑠 ) ∩ 𝑋 ) ∈ 𝐽 } )
14 imassrn ⊢ ( 𝐹 “ 𝑋 ) ⊆ ran 𝐹
15 forn ⊢ ( 𝐹 : 𝑍 –onto→ 𝑌 → ran 𝐹 = 𝑌 )
16 15 3ad2ant2 ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ran 𝐹 = 𝑌 )
17 14 16 sseqtrid ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( 𝐹 “ 𝑋 ) ⊆ 𝑌 )
18 foima ⊢ ( 𝐹 : 𝑍 –onto→ 𝑌 → ( 𝐹 “ 𝑍 ) = 𝑌 )
19 18 3ad2ant2 ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( 𝐹 “ 𝑍 ) = 𝑌 )
20 imass2 ⊢ ( 𝑍 ⊆ 𝑋 → ( 𝐹 “ 𝑍 ) ⊆ ( 𝐹 “ 𝑋 ) )
21 8 20 syl ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( 𝐹 “ 𝑍 ) ⊆ ( 𝐹 “ 𝑋 ) )
22 19 21 eqsstrrd ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → 𝑌 ⊆ ( 𝐹 “ 𝑋 ) )
23 17 22 eqssd ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( 𝐹 “ 𝑋 ) = 𝑌 )
24 23 pweqd ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → 𝒫 ( 𝐹 “ 𝑋 ) = 𝒫 𝑌 )
25 cnvimass ⊢ ( ◡ 𝐹 “ 𝑠 ) ⊆ dom 𝐹
26 25 4 fssdm ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( ◡ 𝐹 “ 𝑠 ) ⊆ 𝑍 )
27 26 8 sstrd ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( ◡ 𝐹 “ 𝑠 ) ⊆ 𝑋 )
28 df-ss ⊢ ( ( ◡ 𝐹 “ 𝑠 ) ⊆ 𝑋 ↔ ( ( ◡ 𝐹 “ 𝑠 ) ∩ 𝑋 ) = ( ◡ 𝐹 “ 𝑠 ) )
29 27 28 sylib ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( ( ◡ 𝐹 “ 𝑠 ) ∩ 𝑋 ) = ( ◡ 𝐹 “ 𝑠 ) )
30 29 eleq1d ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( ( ( ◡ 𝐹 “ 𝑠 ) ∩ 𝑋 ) ∈ 𝐽 ↔ ( ◡ 𝐹 “ 𝑠 ) ∈ 𝐽 ) )
31 24 30 rabeqbidv ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → { 𝑠 ∈ 𝒫 ( 𝐹 “ 𝑋 ) ∣ ( ( ◡ 𝐹 “ 𝑠 ) ∩ 𝑋 ) ∈ 𝐽 } = { 𝑠 ∈ 𝒫 𝑌 ∣ ( ◡ 𝐹 “ 𝑠 ) ∈ 𝐽 } )
32 13 31 eqtrd ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( 𝐽 qTop 𝐹 ) = { 𝑠 ∈ 𝒫 𝑌 ∣ ( ◡ 𝐹 “ 𝑠 ) ∈ 𝐽 } )