Theorem toprestsubel

Description: A subset is open in the topology it generates via restriction. (Contributed by Glauco Siliprandi, 21-Dec-2024)

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

Proof

Step	Hyp	Ref	Expression
1		toprestsubel.1	⊢ ( 𝜑 → 𝐽 ∈ Top )
2		toprestsubel.2	⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝐽 )
3		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
4	3	topopn	⊢ ( 𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽 )
5	1 4	syl	⊢ ( 𝜑 → ∪ 𝐽 ∈ 𝐽 )
6	1 5 2	restsubel	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐽 ↾t 𝐴 ) )