This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ 𝑉 ∧ 𝐽 ⊆ 𝒫 𝐴 ) → ( 𝐽 ↾t 𝐴 ) = 𝐽 )

Proof

Step Hyp Ref Expression
1 pwexg ⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V )
2 1 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐽 ⊆ 𝒫 𝐴 ) → 𝒫 𝐴 ∈ V )
3 simpr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐽 ⊆ 𝒫 𝐴 ) → 𝐽 ⊆ 𝒫 𝐴 )
4 2 3 ssexd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐽 ⊆ 𝒫 𝐴 ) → 𝐽 ∈ V )
5 simpl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐽 ⊆ 𝒫 𝐴 ) → 𝐴 ∈ 𝑉 )
6 restval ⊢ ( ( 𝐽 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) = ran ( 𝑥 ∈ 𝐽 ↦ ( 𝑥 ∩ 𝐴 ) ) )
7 4 5 6 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐽 ⊆ 𝒫 𝐴 ) → ( 𝐽 ↾t 𝐴 ) = ran ( 𝑥 ∈ 𝐽 ↦ ( 𝑥 ∩ 𝐴 ) ) )
8 3 sselda ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐽 ⊆ 𝒫 𝐴 ) ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ∈ 𝒫 𝐴 )
9 8 elpwid ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐽 ⊆ 𝒫 𝐴 ) ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ⊆ 𝐴 )
10 dfss2 ⊢ ( 𝑥 ⊆ 𝐴 ↔ ( 𝑥 ∩ 𝐴 ) = 𝑥 )
11 9 10 sylib ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐽 ⊆ 𝒫 𝐴 ) ∧ 𝑥 ∈ 𝐽 ) → ( 𝑥 ∩ 𝐴 ) = 𝑥 )
12 11 mpteq2dva ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐽 ⊆ 𝒫 𝐴 ) → ( 𝑥 ∈ 𝐽 ↦ ( 𝑥 ∩ 𝐴 ) ) = ( 𝑥 ∈ 𝐽 ↦ 𝑥 ) )
13 mptresid ⊢ ( I ↾ 𝐽 ) = ( 𝑥 ∈ 𝐽 ↦ 𝑥 )
14 12 13 eqtr4di ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐽 ⊆ 𝒫 𝐴 ) → ( 𝑥 ∈ 𝐽 ↦ ( 𝑥 ∩ 𝐴 ) ) = ( I ↾ 𝐽 ) )
15 14 rneqd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐽 ⊆ 𝒫 𝐴 ) → ran ( 𝑥 ∈ 𝐽 ↦ ( 𝑥 ∩ 𝐴 ) ) = ran ( I ↾ 𝐽 ) )
16 rnresi ⊢ ran ( I ↾ 𝐽 ) = 𝐽
17 15 16 eqtrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐽 ⊆ 𝒫 𝐴 ) → ran ( 𝑥 ∈ 𝐽 ↦ ( 𝑥 ∩ 𝐴 ) ) = 𝐽 )
18 7 17 eqtrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐽 ⊆ 𝒫 𝐴 ) → ( 𝐽 ↾t 𝐴 ) = 𝐽 )