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 ⊢ J ↾ 𝑡 A ⊆ 𝒫 A

Proof

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