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 𝑋 ) = 𝐽 )