Metamath Proof Explorer

Theorem resstopn

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

Ref Expression
Hypotheses resstopn.1 ⊢ H = K ↾ 𝑠 A
resstopn.2 ⊢ J = TopOpen ⁡ K
Assertion resstopn ⊢ J ↾ 𝑡 A = TopOpen ⁡ H

Proof

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