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

Metamath Proof Explorer

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 𝐴 ) ⊆ 𝒫 𝐴