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

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 ( ( 𝐾 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐾 ) → ( 𝐽 ↾t 𝐴 ) ⊆ ( 𝐾 ↾t 𝐴 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ) → 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) )
2 ssrexv ⊢ ( 𝐽 ⊆ 𝐾 → ( ∃ 𝑦 ∈ 𝐽 𝑥 = ( 𝑦 ∩ 𝐴 ) → ∃ 𝑦 ∈ 𝐾 𝑥 = ( 𝑦 ∩ 𝐴 ) ) )
3 2 ad2antlr ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ) → ( ∃ 𝑦 ∈ 𝐽 𝑥 = ( 𝑦 ∩ 𝐴 ) → ∃ 𝑦 ∈ 𝐾 𝑥 = ( 𝑦 ∩ 𝐴 ) ) )
4 n0i ⊢ ( 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) → ¬ ( 𝐽 ↾t 𝐴 ) = ∅ )
5 restfn ⊢ ↾t Fn ( V × V )
6 5 fndmi ⊢ dom ↾t = ( V × V )
7 6 ndmov ⊢ ( ¬ ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → ( 𝐽 ↾t 𝐴 ) = ∅ )
8 4 7 nsyl2 ⊢ ( 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) → ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) )
9 8 adantl ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ) → ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) )
10 elrest ⊢ ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ↔ ∃ 𝑦 ∈ 𝐽 𝑥 = ( 𝑦 ∩ 𝐴 ) ) )
11 9 10 syl ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ) → ( 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ↔ ∃ 𝑦 ∈ 𝐽 𝑥 = ( 𝑦 ∩ 𝐴 ) ) )
12 simpll ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ) → 𝐾 ∈ 𝑉 )
13 9 simprd ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ) → 𝐴 ∈ V )
14 elrest ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝐴 ∈ V ) → ( 𝑥 ∈ ( 𝐾 ↾t 𝐴 ) ↔ ∃ 𝑦 ∈ 𝐾 𝑥 = ( 𝑦 ∩ 𝐴 ) ) )
15 12 13 14 syl2anc ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ) → ( 𝑥 ∈ ( 𝐾 ↾t 𝐴 ) ↔ ∃ 𝑦 ∈ 𝐾 𝑥 = ( 𝑦 ∩ 𝐴 ) ) )
16 3 11 15 3imtr4d ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ) → ( 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) → 𝑥 ∈ ( 𝐾 ↾t 𝐴 ) ) )
17 1 16 mpd ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ) → 𝑥 ∈ ( 𝐾 ↾t 𝐴 ) )
18 17 ex ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐾 ) → ( 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) → 𝑥 ∈ ( 𝐾 ↾t 𝐴 ) ) )
19 18 ssrdv ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐾 ) → ( 𝐽 ↾t 𝐴 ) ⊆ ( 𝐾 ↾t 𝐴 ) )