Metamath Proof Explorer

Theorem restid2

Description: The subspace topology over a subset of the base set is the original topology. (Contributed by Mario Carneiro, 13-Aug-2015)

Ref Expression
Assertion restid2 ⊢ A ∈ V ∧ J ⊆ 𝒫 A → J ↾ 𝑡 A = J

Proof

Step Hyp Ref Expression
1 pwexg ⊢ A ∈ V → 𝒫 A ∈ V
2 1 adantr ⊢ A ∈ V ∧ J ⊆ 𝒫 A → 𝒫 A ∈ V
3 simpr ⊢ A ∈ V ∧ J ⊆ 𝒫 A → J ⊆ 𝒫 A
4 2 3 ssexd ⊢ A ∈ V ∧ J ⊆ 𝒫 A → J ∈ V
5 simpl ⊢ A ∈ V ∧ J ⊆ 𝒫 A → A ∈ V
6 restval ⊢ J ∈ V ∧ A ∈ V → J ↾ 𝑡 A = ran ⁡ x ∈ J ⟼ x ∩ A
7 4 5 6 syl2anc ⊢ A ∈ V ∧ J ⊆ 𝒫 A → J ↾ 𝑡 A = ran ⁡ x ∈ J ⟼ x ∩ A
8 3 sselda ⊢ A ∈ V ∧ J ⊆ 𝒫 A ∧ x ∈ J → x ∈ 𝒫 A
9 8 elpwid ⊢ A ∈ V ∧ J ⊆ 𝒫 A ∧ x ∈ J → x ⊆ A
10 dfss2 ⊢ x ⊆ A ↔ x ∩ A = x
11 9 10 sylib ⊢ A ∈ V ∧ J ⊆ 𝒫 A ∧ x ∈ J → x ∩ A = x
12 11 mpteq2dva ⊢ A ∈ V ∧ J ⊆ 𝒫 A → x ∈ J ⟼ x ∩ A = x ∈ J ⟼ x
13 mptresid ⊢ I ↾ J = x ∈ J ⟼ x
14 12 13 eqtr4di ⊢ A ∈ V ∧ J ⊆ 𝒫 A → x ∈ J ⟼ x ∩ A = I ↾ J
15 14 rneqd ⊢ A ∈ V ∧ J ⊆ 𝒫 A → ran ⁡ x ∈ J ⟼ x ∩ A = ran ⁡ I ↾ J
16 rnresi ⊢ ran ⁡ I ↾ J = J
17 15 16 eqtrdi ⊢ A ∈ V ∧ J ⊆ 𝒫 A → ran ⁡ x ∈ J ⟼ x ∩ A = J
18 7 17 eqtrd ⊢ A ∈ V ∧ J ⊆ 𝒫 A → J ↾ 𝑡 A = J