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 eqtrid ⊢ ( 𝐴 ∈ 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 eqtrid ⊢ ( ¬ 𝐴 ∈ 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 ‘ 𝐻 )