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

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 ( 𝐹 ↾ 𝑋 ) ) )