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