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

Metamath Proof Explorer

Theorem 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 𝐹 ) )