# Metamath Proof Explorer

## Theorem qtopres

Description: The quotient topology is unaffected by restriction to the base set. This property makes it slightly more convenient to use, since we don't have to require that F be a function with domain X . (Contributed by Mario Carneiro, 23-Mar-2015)

Ref Expression
Hypothesis qtopval.1 𝑋 = 𝐽
Assertion qtopres ( 𝐹𝑉 → ( 𝐽 qTop 𝐹 ) = ( 𝐽 qTop ( 𝐹𝑋 ) ) )

### Proof

Step Hyp Ref Expression
1 qtopval.1 𝑋 = 𝐽
2 resima ( ( 𝐹𝑋 ) “ 𝑋 ) = ( 𝐹𝑋 )
3 2 pweqi 𝒫 ( ( 𝐹𝑋 ) “ 𝑋 ) = 𝒫 ( 𝐹𝑋 )
4 3 rabeqi { 𝑠 ∈ 𝒫 ( ( 𝐹𝑋 ) “ 𝑋 ) ∣ ( ( ( 𝐹𝑋 ) “ 𝑠 ) ∩ 𝑋 ) ∈ 𝐽 } = { 𝑠 ∈ 𝒫 ( 𝐹𝑋 ) ∣ ( ( ( 𝐹𝑋 ) “ 𝑠 ) ∩ 𝑋 ) ∈ 𝐽 }
5 residm ( ( 𝐹𝑋 ) ↾ 𝑋 ) = ( 𝐹𝑋 )
6 5 cnveqi ( ( 𝐹𝑋 ) ↾ 𝑋 ) = ( 𝐹𝑋 )
7 6 imaeq1i ( ( ( 𝐹𝑋 ) ↾ 𝑋 ) “ 𝑠 ) = ( ( 𝐹𝑋 ) “ 𝑠 )
8 cnvresima ( ( ( 𝐹𝑋 ) ↾ 𝑋 ) “ 𝑠 ) = ( ( ( 𝐹𝑋 ) “ 𝑠 ) ∩ 𝑋 )
9 cnvresima ( ( 𝐹𝑋 ) “ 𝑠 ) = ( ( 𝐹𝑠 ) ∩ 𝑋 )
10 7 8 9 3eqtr3i ( ( ( 𝐹𝑋 ) “ 𝑠 ) ∩ 𝑋 ) = ( ( 𝐹𝑠 ) ∩ 𝑋 )
11 10 eleq1i ( ( ( ( 𝐹𝑋 ) “ 𝑠 ) ∩ 𝑋 ) ∈ 𝐽 ↔ ( ( 𝐹𝑠 ) ∩ 𝑋 ) ∈ 𝐽 )
12 11 rabbii { 𝑠 ∈ 𝒫 ( 𝐹𝑋 ) ∣ ( ( ( 𝐹𝑋 ) “ 𝑠 ) ∩ 𝑋 ) ∈ 𝐽 } = { 𝑠 ∈ 𝒫 ( 𝐹𝑋 ) ∣ ( ( 𝐹𝑠 ) ∩ 𝑋 ) ∈ 𝐽 }
13 4 12 eqtr2i { 𝑠 ∈ 𝒫 ( 𝐹𝑋 ) ∣ ( ( 𝐹𝑠 ) ∩ 𝑋 ) ∈ 𝐽 } = { 𝑠 ∈ 𝒫 ( ( 𝐹𝑋 ) “ 𝑋 ) ∣ ( ( ( 𝐹𝑋 ) “ 𝑠 ) ∩ 𝑋 ) ∈ 𝐽 }
14 1 qtopval ( ( 𝐽 ∈ V ∧ 𝐹𝑉 ) → ( 𝐽 qTop 𝐹 ) = { 𝑠 ∈ 𝒫 ( 𝐹𝑋 ) ∣ ( ( 𝐹𝑠 ) ∩ 𝑋 ) ∈ 𝐽 } )
15 resexg ( 𝐹𝑉 → ( 𝐹𝑋 ) ∈ V )
16 1 qtopval ( ( 𝐽 ∈ V ∧ ( 𝐹𝑋 ) ∈ V ) → ( 𝐽 qTop ( 𝐹𝑋 ) ) = { 𝑠 ∈ 𝒫 ( ( 𝐹𝑋 ) “ 𝑋 ) ∣ ( ( ( 𝐹𝑋 ) “ 𝑠 ) ∩ 𝑋 ) ∈ 𝐽 } )
17 15 16 sylan2 ( ( 𝐽 ∈ V ∧ 𝐹𝑉 ) → ( 𝐽 qTop ( 𝐹𝑋 ) ) = { 𝑠 ∈ 𝒫 ( ( 𝐹𝑋 ) “ 𝑋 ) ∣ ( ( ( 𝐹𝑋 ) “ 𝑠 ) ∩ 𝑋 ) ∈ 𝐽 } )
18 13 14 17 3eqtr4a ( ( 𝐽 ∈ V ∧ 𝐹𝑉 ) → ( 𝐽 qTop 𝐹 ) = ( 𝐽 qTop ( 𝐹𝑋 ) ) )
19 18 expcom ( 𝐹𝑉 → ( 𝐽 ∈ V → ( 𝐽 qTop 𝐹 ) = ( 𝐽 qTop ( 𝐹𝑋 ) ) ) )
20 df-qtop qTop = ( 𝑗 ∈ V , 𝑓 ∈ V ↦ { 𝑠 ∈ 𝒫 ( 𝑓 𝑗 ) ∣ ( ( 𝑓𝑠 ) ∩ 𝑗 ) ∈ 𝑗 } )
21 20 reldmmpo Rel dom qTop
22 21 ovprc1 ( ¬ 𝐽 ∈ V → ( 𝐽 qTop 𝐹 ) = ∅ )
23 21 ovprc1 ( ¬ 𝐽 ∈ V → ( 𝐽 qTop ( 𝐹𝑋 ) ) = ∅ )
24 22 23 eqtr4d ( ¬ 𝐽 ∈ V → ( 𝐽 qTop 𝐹 ) = ( 𝐽 qTop ( 𝐹𝑋 ) ) )
25 19 24 pm2.61d1 ( 𝐹𝑉 → ( 𝐽 qTop 𝐹 ) = ( 𝐽 qTop ( 𝐹𝑋 ) ) )