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 4 9 fexd ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → 𝐹 ∈ V )
11 1 qtopval ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 ∈ V ) → ( 𝐽 qTop 𝐹 ) = { 𝑠 ∈ 𝒫 ( 𝐹 “ 𝑋 ) ∣ ( ( ◡ 𝐹 “ 𝑠 ) ∩ 𝑋 ) ∈ 𝐽 } )
12 2 10 11 syl2anc ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( 𝐽 qTop 𝐹 ) = { 𝑠 ∈ 𝒫 ( 𝐹 “ 𝑋 ) ∣ ( ( ◡ 𝐹 “ 𝑠 ) ∩ 𝑋 ) ∈ 𝐽 } )
13 imassrn ⊢ ( 𝐹 “ 𝑋 ) ⊆ ran 𝐹
14 forn ⊢ ( 𝐹 : 𝑍 –onto→ 𝑌 → ran 𝐹 = 𝑌 )
15 14 3ad2ant2 ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ran 𝐹 = 𝑌 )
16 13 15 sseqtrid ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( 𝐹 “ 𝑋 ) ⊆ 𝑌 )
17 foima ⊢ ( 𝐹 : 𝑍 –onto→ 𝑌 → ( 𝐹 “ 𝑍 ) = 𝑌 )
18 17 3ad2ant2 ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( 𝐹 “ 𝑍 ) = 𝑌 )
19 imass2 ⊢ ( 𝑍 ⊆ 𝑋 → ( 𝐹 “ 𝑍 ) ⊆ ( 𝐹 “ 𝑋 ) )
20 8 19 syl ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( 𝐹 “ 𝑍 ) ⊆ ( 𝐹 “ 𝑋 ) )
21 18 20 eqsstrrd ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → 𝑌 ⊆ ( 𝐹 “ 𝑋 ) )
22 16 21 eqssd ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( 𝐹 “ 𝑋 ) = 𝑌 )
23 22 pweqd ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → 𝒫 ( 𝐹 “ 𝑋 ) = 𝒫 𝑌 )
24 cnvimass ⊢ ( ◡ 𝐹 “ 𝑠 ) ⊆ dom 𝐹
25 24 4 fssdm ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( ◡ 𝐹 “ 𝑠 ) ⊆ 𝑍 )
26 25 8 sstrd ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( ◡ 𝐹 “ 𝑠 ) ⊆ 𝑋 )
27 dfss2 ⊢ ( ( ◡ 𝐹 “ 𝑠 ) ⊆ 𝑋 ↔ ( ( ◡ 𝐹 “ 𝑠 ) ∩ 𝑋 ) = ( ◡ 𝐹 “ 𝑠 ) )
28 26 27 sylib ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( ( ◡ 𝐹 “ 𝑠 ) ∩ 𝑋 ) = ( ◡ 𝐹 “ 𝑠 ) )
29 28 eleq1d ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( ( ( ◡ 𝐹 “ 𝑠 ) ∩ 𝑋 ) ∈ 𝐽 ↔ ( ◡ 𝐹 “ 𝑠 ) ∈ 𝐽 ) )
30 23 29 rabeqbidv ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → { 𝑠 ∈ 𝒫 ( 𝐹 “ 𝑋 ) ∣ ( ( ◡ 𝐹 “ 𝑠 ) ∩ 𝑋 ) ∈ 𝐽 } = { 𝑠 ∈ 𝒫 𝑌 ∣ ( ◡ 𝐹 “ 𝑠 ) ∈ 𝐽 } )
31 12 30 eqtrd ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( 𝐽 qTop 𝐹 ) = { 𝑠 ∈ 𝒫 𝑌 ∣ ( ◡ 𝐹 “ 𝑠 ) ∈ 𝐽 } )