Metamath Proof Explorer

Theorem resttopon

Description: A subspace topology is a topology on the base set. (Contributed by Mario Carneiro, 13-Aug-2015)

Ref Expression
Assertion resttopon ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → J ↾ 𝑡 A ∈ TopOn ⁡ A

Proof

Step Hyp Ref Expression
1 topontop ⊢ J ∈ TopOn ⁡ X → J ∈ Top
2 id ⊢ A ⊆ X → A ⊆ X
3 toponmax ⊢ J ∈ TopOn ⁡ X → X ∈ J
4 ssexg ⊢ A ⊆ X ∧ X ∈ J → A ∈ V
5 2 3 4 syl2anr ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → A ∈ V
6 resttop ⊢ J ∈ Top ∧ A ∈ V → J ↾ 𝑡 A ∈ Top
7 1 5 6 syl2an2r ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → J ↾ 𝑡 A ∈ Top
8 sseqin2 ⊢ A ⊆ X ↔ X ∩ A = A
9 8 bilani ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → X ∩ A = A
10 simpl ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → J ∈ TopOn ⁡ X
11 3 adantr ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → X ∈ J
12 elrestr ⊢ J ∈ TopOn ⁡ X ∧ A ∈ V ∧ X ∈ J → X ∩ A ∈ J ↾ 𝑡 A
13 10 5 11 12 syl3anc ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → X ∩ A ∈ J ↾ 𝑡 A
14 9 13 eqeltrrd ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → A ∈ J ↾ 𝑡 A
15 elssuni ⊢ A ∈ J ↾ 𝑡 A → A ⊆ ⋃ J ↾ 𝑡 A
16 14 15 syl ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → A ⊆ ⋃ J ↾ 𝑡 A
17 restval ⊢ J ∈ TopOn ⁡ X ∧ A ∈ V → J ↾ 𝑡 A = ran ⁡ x ∈ J ⟼ x ∩ A
18 5 17 syldan ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → J ↾ 𝑡 A = ran ⁡ x ∈ J ⟼ x ∩ A
19 inss2 ⊢ x ∩ A ⊆ A
20 vex ⊢ x ∈ V
21 20 inex1 ⊢ x ∩ A ∈ V
22 21 elpw ⊢ x ∩ A ∈ 𝒫 A ↔ x ∩ A ⊆ A
23 19 22 mpbir ⊢ x ∩ A ∈ 𝒫 A
24 23 a1i ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X ∧ x ∈ J → x ∩ A ∈ 𝒫 A
25 24 fmpttd ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → x ∈ J ⟼ x ∩ A : J ⟶ 𝒫 A
26 25 frnd ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → ran ⁡ x ∈ J ⟼ x ∩ A ⊆ 𝒫 A
27 18 26 eqsstrd ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → J ↾ 𝑡 A ⊆ 𝒫 A
28 sspwuni ⊢ J ↾ 𝑡 A ⊆ 𝒫 A ↔ ⋃ J ↾ 𝑡 A ⊆ A
29 27 28 sylib ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → ⋃ J ↾ 𝑡 A ⊆ A
30 16 29 eqssd ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → A = ⋃ J ↾ 𝑡 A
31 istopon ⊢ J ↾ 𝑡 A ∈ TopOn ⁡ A ↔ J ↾ 𝑡 A ∈ Top ∧ A = ⋃ J ↾ 𝑡 A
32 7 30 31 sylanbrc ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → J ↾ 𝑡 A ∈ TopOn ⁡ A