Theorem restsspw

Description: The subspace topology is a collection of subsets of the restriction set. (Contributed by Mario Carneiro, 13-Aug-2015)

	Ref	Expression
Assertion	restsspw	⊢ ( 𝐽 ↾t 𝐴 ) ⊆ 𝒫 𝐴

Proof

Step	Hyp	Ref	Expression
1		n0i	⊢ ( 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) → ¬ ( 𝐽 ↾t 𝐴 ) = ∅ )
2		restfn	⊢ ↾t Fn ( V × V )
3		fndm	⊢ ( ↾t Fn ( V × V ) → dom ↾t = ( V × V ) )
4	2 3	ax-mp	⊢ dom ↾t = ( V × V )
5	4	ndmov	⊢ ( ¬ ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → ( 𝐽 ↾t 𝐴 ) = ∅ )
6	1 5	nsyl2	⊢ ( 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) → ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) )
7		elrest	⊢ ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ↔ ∃ 𝑦 ∈ 𝐽 𝑥 = ( 𝑦 ∩ 𝐴 ) ) )
8	6 7	syl	⊢ ( 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) → ( 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ↔ ∃ 𝑦 ∈ 𝐽 𝑥 = ( 𝑦 ∩ 𝐴 ) ) )
9	8	ibi	⊢ ( 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) → ∃ 𝑦 ∈ 𝐽 𝑥 = ( 𝑦 ∩ 𝐴 ) )
10		inss2	⊢ ( 𝑦 ∩ 𝐴 ) ⊆ 𝐴
11		sseq1	⊢ ( 𝑥 = ( 𝑦 ∩ 𝐴 ) → ( 𝑥 ⊆ 𝐴 ↔ ( 𝑦 ∩ 𝐴 ) ⊆ 𝐴 ) )
12	10 11	mpbiri	⊢ ( 𝑥 = ( 𝑦 ∩ 𝐴 ) → 𝑥 ⊆ 𝐴 )
13	12	rexlimivw	⊢ ( ∃ 𝑦 ∈ 𝐽 𝑥 = ( 𝑦 ∩ 𝐴 ) → 𝑥 ⊆ 𝐴 )
14	9 13	syl	⊢ ( 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) → 𝑥 ⊆ 𝐴 )
15		velpw	⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
16	14 15	sylibr	⊢ ( 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) → 𝑥 ∈ 𝒫 𝐴 )
17	16	ssriv	⊢ ( 𝐽 ↾t 𝐴 ) ⊆ 𝒫 𝐴