Metamath Proof Explorer

Theorem iscnrm3lem1

Description: Lemma for iscnrm3 . Subspace topology is a topology. (Contributed by Zhi Wang, 3-Sep-2024)

Ref Expression
Assertion iscnrm3lem1 ⊢ J ∈ Top → ∀ x ∈ A φ ↔ ∀ x ∈ A J ↾ 𝑡 x ∈ Top ∧ φ

Proof

Step Hyp Ref Expression
1 resttop ⊢ J ∈ Top ∧ x ∈ A → J ↾ 𝑡 x ∈ Top
2 1 biantrurd ⊢ J ∈ Top ∧ x ∈ A → φ ↔ J ↾ 𝑡 x ∈ Top ∧ φ
3 2 ralbidva ⊢ J ∈ Top → ∀ x ∈ A φ ↔ ∀ x ∈ A J ↾ 𝑡 x ∈ Top ∧ φ