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