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 fndm ( ↾t Fn ( V × V ) → dom ↾t = ( V × V ) )
7 5 6 ax-mp dom ↾t = ( V × V )
8 7 ndmov ( ¬ ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → ( 𝐽t 𝐴 ) = ∅ )
9 4 8 nsyl2 ( 𝑥 ∈ ( 𝐽t 𝐴 ) → ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) )
10 9 adantl ( ( ( 𝐾𝑉𝐽𝐾 ) ∧ 𝑥 ∈ ( 𝐽t 𝐴 ) ) → ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) )
11 elrest ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑥 ∈ ( 𝐽t 𝐴 ) ↔ ∃ 𝑦𝐽 𝑥 = ( 𝑦𝐴 ) ) )
12 10 11 syl ( ( ( 𝐾𝑉𝐽𝐾 ) ∧ 𝑥 ∈ ( 𝐽t 𝐴 ) ) → ( 𝑥 ∈ ( 𝐽t 𝐴 ) ↔ ∃ 𝑦𝐽 𝑥 = ( 𝑦𝐴 ) ) )
13 simpll ( ( ( 𝐾𝑉𝐽𝐾 ) ∧ 𝑥 ∈ ( 𝐽t 𝐴 ) ) → 𝐾𝑉 )
14 10 simprd ( ( ( 𝐾𝑉𝐽𝐾 ) ∧ 𝑥 ∈ ( 𝐽t 𝐴 ) ) → 𝐴 ∈ V )
15 elrest ( ( 𝐾𝑉𝐴 ∈ V ) → ( 𝑥 ∈ ( 𝐾t 𝐴 ) ↔ ∃ 𝑦𝐾 𝑥 = ( 𝑦𝐴 ) ) )
16 13 14 15 syl2anc ( ( ( 𝐾𝑉𝐽𝐾 ) ∧ 𝑥 ∈ ( 𝐽t 𝐴 ) ) → ( 𝑥 ∈ ( 𝐾t 𝐴 ) ↔ ∃ 𝑦𝐾 𝑥 = ( 𝑦𝐴 ) ) )
17 3 12 16 3imtr4d ( ( ( 𝐾𝑉𝐽𝐾 ) ∧ 𝑥 ∈ ( 𝐽t 𝐴 ) ) → ( 𝑥 ∈ ( 𝐽t 𝐴 ) → 𝑥 ∈ ( 𝐾t 𝐴 ) ) )
18 1 17 mpd ( ( ( 𝐾𝑉𝐽𝐾 ) ∧ 𝑥 ∈ ( 𝐽t 𝐴 ) ) → 𝑥 ∈ ( 𝐾t 𝐴 ) )
19 18 ex ( ( 𝐾𝑉𝐽𝐾 ) → ( 𝑥 ∈ ( 𝐽t 𝐴 ) → 𝑥 ∈ ( 𝐾t 𝐴 ) ) )
20 19 ssrdv ( ( 𝐾𝑉𝐽𝐾 ) → ( 𝐽t 𝐴 ) ⊆ ( 𝐾t 𝐴 ) )