Theorem restopnssd

Description: A topology restricted to an open set is a subset of the original topology. (Contributed by Glauco Siliprandi, 21-Dec-2024)

	Ref	Expression
Hypotheses	restopnssd.1	⊢ ( 𝜑 → 𝐽 ∈ Top )
	restopnssd.2	⊢ ( 𝜑 → 𝐴 ∈ 𝐽 )
Assertion	restopnssd	⊢ ( 𝜑 → ( 𝐽 ↾t 𝐴 ) ⊆ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		restopnssd.1	⊢ ( 𝜑 → 𝐽 ∈ Top )
2		restopnssd.2	⊢ ( 𝜑 → 𝐴 ∈ 𝐽 )
3		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ) → 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) )
4	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ) → 𝐽 ∈ Top )
5	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ) → 𝐴 ∈ 𝐽 )
6		restopn2	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ) → ( 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ↔ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐴 ) ) )
7	4 5 6	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ) → ( 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ↔ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐴 ) ) )
8	3 7	mpbid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ) → ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐴 ) )
9	8	simpld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ) → 𝑥 ∈ 𝐽 )
10	9	ssd	⊢ ( 𝜑 → ( 𝐽 ↾t 𝐴 ) ⊆ 𝐽 )