Theorem restt1

Description: A subspace of a T_1 topology is T_1. (Contributed by Mario Carneiro, 25-Aug-2015)

	Ref	Expression
Assertion	restt1	⊢ ( ( 𝐽 ∈ Fre ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) ∈ Fre )

Proof

Step	Hyp	Ref	Expression
1		t1top	⊢ ( 𝐽 ∈ Fre → 𝐽 ∈ Top )
2		cnt1	⊢ ( ( 𝐽 ∈ Fre ∧ ( I ↾ ( 𝐴 ∩ ∪ 𝐽 ) ) : ( 𝐴 ∩ ∪ 𝐽 ) –1-1→ ( 𝐴 ∩ ∪ 𝐽 ) ∧ ( I ↾ ( 𝐴 ∩ ∪ 𝐽 ) ) ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐽 ) ) → ( 𝐽 ↾t 𝐴 ) ∈ Fre )
3	1 2	resthauslem	⊢ ( ( 𝐽 ∈ Fre ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) ∈ Fre )