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

Metamath Proof Explorer

Theorem restid

Description: The subspace topology of the base set is the original topology. (Contributed by Jeff Hankins, 9-Jul-2009) (Revised by Mario Carneiro, 13-Aug-2015)

Ref Expression
Hypothesis restid.1 ⊢ 𝑋 = ∪ 𝐽
Assertion restid ( 𝐽 ∈ 𝑉 → ( 𝐽 ↾t 𝑋 ) = 𝐽 )

Proof

Step Hyp Ref Expression
1 restid.1 ⊢ 𝑋 = ∪ 𝐽
2 uniexg ⊢ ( 𝐽 ∈ 𝑉 → ∪ 𝐽 ∈ V )
3 1 2 eqeltrid ⊢ ( 𝐽 ∈ 𝑉 → 𝑋 ∈ V )
4 1 eqimss2i ⊢ ∪ 𝐽 ⊆ 𝑋
5 sspwuni ⊢ ( 𝐽 ⊆ 𝒫 𝑋 ↔ ∪ 𝐽 ⊆ 𝑋 )
6 4 5 mpbir ⊢ 𝐽 ⊆ 𝒫 𝑋
7 restid2 ⊢ ( ( 𝑋 ∈ V ∧ 𝐽 ⊆ 𝒫 𝑋 ) → ( 𝐽 ↾t 𝑋 ) = 𝐽 )
8 3 6 7 sylancl ⊢ ( 𝐽 ∈ 𝑉 → ( 𝐽 ↾t 𝑋 ) = 𝐽 )