Metamath Proof Explorer

Theorem ssrest

Description: If K is a finer topology than J , then the subspace topologies induced by A maintain this relationship. (Contributed by Mario Carneiro, 21-Mar-2015) (Revised by Mario Carneiro, 1-May-2015)

Ref Expression
Assertion ssrest ⊢ K ∈ V ∧ J ⊆ K → J ↾ 𝑡 A ⊆ K ↾ 𝑡 A

Proof

Step Hyp Ref Expression
1 simpr ⊢ K ∈ V ∧ J ⊆ K ∧ x ∈ J ↾ 𝑡 A → x ∈ J ↾ 𝑡 A
2 ssrexv ⊢ J ⊆ K → ∃ y ∈ J x = y ∩ A → ∃ y ∈ K x = y ∩ A
3 2 ad2antlr ⊢ K ∈ V ∧ J ⊆ K ∧ x ∈ J ↾ 𝑡 A → ∃ y ∈ J x = y ∩ A → ∃ y ∈ K x = y ∩ A
4 n0i ⊢ x ∈ J ↾ 𝑡 A → ¬ J ↾ 𝑡 A = ∅
5 restfn ⊢ ↾ 𝑡 Fn V × V
6 5 fndmi ⊢ dom ⁡ ↾ 𝑡 = V × V
7 6 ndmov ⊢ ¬ J ∈ V ∧ A ∈ V → J ↾ 𝑡 A = ∅
8 4 7 nsyl2 ⊢ x ∈ J ↾ 𝑡 A → J ∈ V ∧ A ∈ V
9 8 adantl ⊢ K ∈ V ∧ J ⊆ K ∧ x ∈ J ↾ 𝑡 A → J ∈ V ∧ A ∈ V
10 elrest ⊢ J ∈ V ∧ A ∈ V → x ∈ J ↾ 𝑡 A ↔ ∃ y ∈ J x = y ∩ A
11 9 10 syl ⊢ K ∈ V ∧ J ⊆ K ∧ x ∈ J ↾ 𝑡 A → x ∈ J ↾ 𝑡 A ↔ ∃ y ∈ J x = y ∩ A
12 simpll ⊢ K ∈ V ∧ J ⊆ K ∧ x ∈ J ↾ 𝑡 A → K ∈ V
13 9 simprd ⊢ K ∈ V ∧ J ⊆ K ∧ x ∈ J ↾ 𝑡 A → A ∈ V
14 elrest ⊢ K ∈ V ∧ A ∈ V → x ∈ K ↾ 𝑡 A ↔ ∃ y ∈ K x = y ∩ A
15 12 13 14 syl2anc ⊢ K ∈ V ∧ J ⊆ K ∧ x ∈ J ↾ 𝑡 A → x ∈ K ↾ 𝑡 A ↔ ∃ y ∈ K x = y ∩ A
16 3 11 15 3imtr4d ⊢ K ∈ V ∧ J ⊆ K ∧ x ∈ J ↾ 𝑡 A → x ∈ J ↾ 𝑡 A → x ∈ K ↾ 𝑡 A
17 1 16 mpd ⊢ K ∈ V ∧ J ⊆ K ∧ x ∈ J ↾ 𝑡 A → x ∈ K ↾ 𝑡 A
18 17 ex ⊢ K ∈ V ∧ J ⊆ K → x ∈ J ↾ 𝑡 A → x ∈ K ↾ 𝑡 A
19 18 ssrdv ⊢ K ∈ V ∧ J ⊆ K → J ↾ 𝑡 A ⊆ K ↾ 𝑡 A