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 simpr ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → A ⊆ X
9 sseqin2 ⊢ A ⊆ X ↔ X ∩ A = A
10 8 9 sylib ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → X ∩ A = A
11 simpl ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → J ∈ TopOn ⁡ X
12 3 adantr ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → X ∈ J
13 elrestr ⊢ J ∈ TopOn ⁡ X ∧ A ∈ V ∧ X ∈ J → X ∩ A ∈ J ↾ 𝑡 A
14 11 5 12 13 syl3anc ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → X ∩ A ∈ J ↾ 𝑡 A
15 10 14 eqeltrrd ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → A ∈ J ↾ 𝑡 A
16 elssuni ⊢ A ∈ J ↾ 𝑡 A → A ⊆ ⋃ J ↾ 𝑡 A
17 15 16 syl ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → A ⊆ ⋃ J ↾ 𝑡 A
18 restval ⊢ J ∈ TopOn ⁡ X ∧ A ∈ V → J ↾ 𝑡 A = ran ⁡ x ∈ J ⟼ x ∩ A
19 5 18 syldan ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → J ↾ 𝑡 A = ran ⁡ x ∈ J ⟼ x ∩ A
20 inss2 ⊢ x ∩ A ⊆ A
21 vex ⊢ x ∈ V
22 21 inex1 ⊢ x ∩ A ∈ V
23 22 elpw ⊢ x ∩ A ∈ 𝒫 A ↔ x ∩ A ⊆ A
24 20 23 mpbir ⊢ x ∩ A ∈ 𝒫 A
25 24 a1i ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X ∧ x ∈ J → x ∩ A ∈ 𝒫 A
26 25 fmpttd ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → x ∈ J ⟼ x ∩ A : J ⟶ 𝒫 A
27 26 frnd ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → ran ⁡ x ∈ J ⟼ x ∩ A ⊆ 𝒫 A
28 19 27 eqsstrd ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → J ↾ 𝑡 A ⊆ 𝒫 A
29 sspwuni ⊢ J ↾ 𝑡 A ⊆ 𝒫 A ↔ ⋃ J ↾ 𝑡 A ⊆ A
30 28 29 sylib ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → ⋃ J ↾ 𝑡 A ⊆ A
31 17 30 eqssd ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → A = ⋃ J ↾ 𝑡 A
32 istopon ⊢ J ↾ 𝑡 A ∈ TopOn ⁡ A ↔ J ↾ 𝑡 A ∈ Top ∧ A = ⋃ J ↾ 𝑡 A
33 7 31 32 sylanbrc ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → J ↾ 𝑡 A ∈ TopOn ⁡ A