Description: Lemma for iscnrm3 . Subspace topology is a topology. (Contributed by Zhi Wang, 3-Sep-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | iscnrm3lem1 | ⊢ ( 𝐽 ∈ Top → ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝐽 ↾t 𝑥 ) ∈ Top ∧ 𝜑 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | resttop | ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐴 ) → ( 𝐽 ↾t 𝑥 ) ∈ Top ) | |
2 | 1 | biantrurd | ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐴 ) → ( 𝜑 ↔ ( ( 𝐽 ↾t 𝑥 ) ∈ Top ∧ 𝜑 ) ) ) |
3 | 2 | ralbidva | ⊢ ( 𝐽 ∈ Top → ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝐽 ↾t 𝑥 ) ∈ Top ∧ 𝜑 ) ) ) |