imastopn

Description: The topology of an image structure. (Contributed by Mario Carneiro, 27-Aug-2015)

	Ref	Expression
Hypotheses	imastps.u	⊢ ( 𝜑 → 𝑈 = ( 𝐹 “_s 𝑅 ) )
	imastps.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
	imastps.f	⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
	imastopn.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
	imastopn.j	⊢ 𝐽 = ( TopOpen ‘ 𝑅 )
	imastopn.o	⊢ 𝑂 = ( TopOpen ‘ 𝑈 )
Assertion	imastopn	⊢ ( 𝜑 → 𝑂 = ( 𝐽 qTop 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		imastps.u	⊢ ( 𝜑 → 𝑈 = ( 𝐹 “_s 𝑅 ) )
2		imastps.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3		imastps.f	⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
4		imastopn.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
5		imastopn.j	⊢ 𝐽 = ( TopOpen ‘ 𝑅 )
6		imastopn.o	⊢ 𝑂 = ( TopOpen ‘ 𝑈 )
7		eqid	⊢ ( TopSet ‘ 𝑈 ) = ( TopSet ‘ 𝑈 )
8	1 2 3 4 5 7	imastset	⊢ ( 𝜑 → ( TopSet ‘ 𝑈 ) = ( 𝐽 qTop 𝐹 ) )
9	5	fvexi	⊢ 𝐽 ∈ V
10		fofn	⊢ ( 𝐹 : 𝑉 –onto→ 𝐵 → 𝐹 Fn 𝑉 )
11	3 10	syl	⊢ ( 𝜑 → 𝐹 Fn 𝑉 )
12		fvex	⊢ ( Base ‘ 𝑅 ) ∈ V
13	2 12	eqeltrdi	⊢ ( 𝜑 → 𝑉 ∈ V )
14		fnex	⊢ ( ( 𝐹 Fn 𝑉 ∧ 𝑉 ∈ V ) → 𝐹 ∈ V )
15	11 13 14	syl2anc	⊢ ( 𝜑 → 𝐹 ∈ V )
16		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
17	16	qtopval	⊢ ( ( 𝐽 ∈ V ∧ 𝐹 ∈ V ) → ( 𝐽 qTop 𝐹 ) = { 𝑥 ∈ 𝒫 ( 𝐹 “ ∪ 𝐽 ) ∣ ( ( ^◡ 𝐹 “ 𝑥 ) ∩ ∪ 𝐽 ) ∈ 𝐽 } )
18	9 15 17	sylancr	⊢ ( 𝜑 → ( 𝐽 qTop 𝐹 ) = { 𝑥 ∈ 𝒫 ( 𝐹 “ ∪ 𝐽 ) ∣ ( ( ^◡ 𝐹 “ 𝑥 ) ∩ ∪ 𝐽 ) ∈ 𝐽 } )
19	8 18	eqtrd	⊢ ( 𝜑 → ( TopSet ‘ 𝑈 ) = { 𝑥 ∈ 𝒫 ( 𝐹 “ ∪ 𝐽 ) ∣ ( ( ^◡ 𝐹 “ 𝑥 ) ∩ ∪ 𝐽 ) ∈ 𝐽 } )
20		ssrab2	⊢ { 𝑥 ∈ 𝒫 ( 𝐹 “ ∪ 𝐽 ) ∣ ( ( ^◡ 𝐹 “ 𝑥 ) ∩ ∪ 𝐽 ) ∈ 𝐽 } ⊆ 𝒫 ( 𝐹 “ ∪ 𝐽 )
21		imassrn	⊢ ( 𝐹 “ ∪ 𝐽 ) ⊆ ran 𝐹
22		forn	⊢ ( 𝐹 : 𝑉 –onto→ 𝐵 → ran 𝐹 = 𝐵 )
23	3 22	syl	⊢ ( 𝜑 → ran 𝐹 = 𝐵 )
24	1 2 3 4	imasbas	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑈 ) )
25	23 24	eqtrd	⊢ ( 𝜑 → ran 𝐹 = ( Base ‘ 𝑈 ) )
26	21 25	sseqtrid	⊢ ( 𝜑 → ( 𝐹 “ ∪ 𝐽 ) ⊆ ( Base ‘ 𝑈 ) )
27	26	sspwd	⊢ ( 𝜑 → 𝒫 ( 𝐹 “ ∪ 𝐽 ) ⊆ 𝒫 ( Base ‘ 𝑈 ) )
28	20 27	sstrid	⊢ ( 𝜑 → { 𝑥 ∈ 𝒫 ( 𝐹 “ ∪ 𝐽 ) ∣ ( ( ^◡ 𝐹 “ 𝑥 ) ∩ ∪ 𝐽 ) ∈ 𝐽 } ⊆ 𝒫 ( Base ‘ 𝑈 ) )
29	19 28	eqsstrd	⊢ ( 𝜑 → ( TopSet ‘ 𝑈 ) ⊆ 𝒫 ( Base ‘ 𝑈 ) )
30		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
31	30 7	topnid	⊢ ( ( TopSet ‘ 𝑈 ) ⊆ 𝒫 ( Base ‘ 𝑈 ) → ( TopSet ‘ 𝑈 ) = ( TopOpen ‘ 𝑈 ) )
32	29 31	syl	⊢ ( 𝜑 → ( TopSet ‘ 𝑈 ) = ( TopOpen ‘ 𝑈 ) )
33	32 6	eqtr4di	⊢ ( 𝜑 → ( TopSet ‘ 𝑈 ) = 𝑂 )
34	33 8	eqtr3d	⊢ ( 𝜑 → 𝑂 = ( 𝐽 qTop 𝐹 ) )

Metamath Proof Explorer

Theorem imastopn

Proof