Metamath Proof Explorer


Theorem resstopn

Description: The topology of a restricted structure. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Hypotheses resstopn.1 𝐻 = ( 𝐾s 𝐴 )
resstopn.2 𝐽 = ( TopOpen ‘ 𝐾 )
Assertion resstopn ( 𝐽t 𝐴 ) = ( TopOpen ‘ 𝐻 )

Proof

Step Hyp Ref Expression
1 resstopn.1 𝐻 = ( 𝐾s 𝐴 )
2 resstopn.2 𝐽 = ( TopOpen ‘ 𝐾 )
3 fvex ( TopSet ‘ 𝐾 ) ∈ V
4 fvex ( Base ‘ 𝐾 ) ∈ V
5 restco ( ( ( TopSet ‘ 𝐾 ) ∈ V ∧ ( Base ‘ 𝐾 ) ∈ V ∧ 𝐴 ∈ V ) → ( ( ( TopSet ‘ 𝐾 ) ↾t ( Base ‘ 𝐾 ) ) ↾t 𝐴 ) = ( ( TopSet ‘ 𝐾 ) ↾t ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) )
6 3 4 5 mp3an12 ( 𝐴 ∈ V → ( ( ( TopSet ‘ 𝐾 ) ↾t ( Base ‘ 𝐾 ) ) ↾t 𝐴 ) = ( ( TopSet ‘ 𝐾 ) ↾t ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) )
7 eqid ( TopSet ‘ 𝐾 ) = ( TopSet ‘ 𝐾 )
8 1 7 resstset ( 𝐴 ∈ V → ( TopSet ‘ 𝐾 ) = ( TopSet ‘ 𝐻 ) )
9 incom ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) = ( 𝐴 ∩ ( Base ‘ 𝐾 ) )
10 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
11 1 10 ressbas ( 𝐴 ∈ V → ( 𝐴 ∩ ( Base ‘ 𝐾 ) ) = ( Base ‘ 𝐻 ) )
12 9 11 syl5eq ( 𝐴 ∈ V → ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) = ( Base ‘ 𝐻 ) )
13 8 12 oveq12d ( 𝐴 ∈ V → ( ( TopSet ‘ 𝐾 ) ↾t ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) = ( ( TopSet ‘ 𝐻 ) ↾t ( Base ‘ 𝐻 ) ) )
14 6 13 eqtrd ( 𝐴 ∈ V → ( ( ( TopSet ‘ 𝐾 ) ↾t ( Base ‘ 𝐾 ) ) ↾t 𝐴 ) = ( ( TopSet ‘ 𝐻 ) ↾t ( Base ‘ 𝐻 ) ) )
15 10 7 topnval ( ( TopSet ‘ 𝐾 ) ↾t ( Base ‘ 𝐾 ) ) = ( TopOpen ‘ 𝐾 )
16 15 2 eqtr4i ( ( TopSet ‘ 𝐾 ) ↾t ( Base ‘ 𝐾 ) ) = 𝐽
17 16 oveq1i ( ( ( TopSet ‘ 𝐾 ) ↾t ( Base ‘ 𝐾 ) ) ↾t 𝐴 ) = ( 𝐽t 𝐴 )
18 eqid ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
19 eqid ( TopSet ‘ 𝐻 ) = ( TopSet ‘ 𝐻 )
20 18 19 topnval ( ( TopSet ‘ 𝐻 ) ↾t ( Base ‘ 𝐻 ) ) = ( TopOpen ‘ 𝐻 )
21 14 17 20 3eqtr3g ( 𝐴 ∈ V → ( 𝐽t 𝐴 ) = ( TopOpen ‘ 𝐻 ) )
22 simpr ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → 𝐴 ∈ V )
23 restfn t Fn ( V × V )
24 23 fndmi dom ↾t = ( V × V )
25 24 ndmov ( ¬ ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → ( 𝐽t 𝐴 ) = ∅ )
26 22 25 nsyl5 ( ¬ 𝐴 ∈ V → ( 𝐽t 𝐴 ) = ∅ )
27 reldmress Rel dom ↾s
28 27 ovprc2 ( ¬ 𝐴 ∈ V → ( 𝐾s 𝐴 ) = ∅ )
29 1 28 syl5eq ( ¬ 𝐴 ∈ V → 𝐻 = ∅ )
30 29 fveq2d ( ¬ 𝐴 ∈ V → ( TopSet ‘ 𝐻 ) = ( TopSet ‘ ∅ ) )
31 tsetid TopSet = Slot ( TopSet ‘ ndx )
32 31 str0 ∅ = ( TopSet ‘ ∅ )
33 30 32 eqtr4di ( ¬ 𝐴 ∈ V → ( TopSet ‘ 𝐻 ) = ∅ )
34 33 oveq1d ( ¬ 𝐴 ∈ V → ( ( TopSet ‘ 𝐻 ) ↾t ( Base ‘ 𝐻 ) ) = ( ∅ ↾t ( Base ‘ 𝐻 ) ) )
35 0rest ( ∅ ↾t ( Base ‘ 𝐻 ) ) = ∅
36 34 20 35 3eqtr3g ( ¬ 𝐴 ∈ V → ( TopOpen ‘ 𝐻 ) = ∅ )
37 26 36 eqtr4d ( ¬ 𝐴 ∈ V → ( 𝐽t 𝐴 ) = ( TopOpen ‘ 𝐻 ) )
38 21 37 pm2.61i ( 𝐽t 𝐴 ) = ( TopOpen ‘ 𝐻 )