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		df-ss	⊢ ( 𝑥 ⊆ 𝐴 ↔ ( 𝑥 ∩ 𝐴 ) = 𝑥 )
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 𝐴 ) = 𝐽 )