Metamath Proof Explorer


Theorem iscnrm3rlem7

Description: Lemma for iscnrm3rlem8 . Open neighborhoods in the subspace topology are open neighborhoods in the original topology given that the subspace is an open set in the original topology. (Contributed by Zhi Wang, 5-Sep-2024)

Ref Expression
Hypotheses iscnrm3rlem4.1 φ J Top
iscnrm3rlem4.2 φ S J
iscnrm3rlem5.3 φ T J
iscnrm3rlem7.4 φ O J 𝑡 J cls J S cls J T
Assertion iscnrm3rlem7 φ O J

Proof

Step Hyp Ref Expression
1 iscnrm3rlem4.1 φ J Top
2 iscnrm3rlem4.2 φ S J
3 iscnrm3rlem5.3 φ T J
4 iscnrm3rlem7.4 φ O J 𝑡 J cls J S cls J T
5 1 uniexd φ J V
6 5 difexd φ J cls J S cls J T V
7 resttop J Top J cls J S cls J T V J 𝑡 J cls J S cls J T Top
8 1 6 7 syl2anc φ J 𝑡 J cls J S cls J T Top
9 eqid J 𝑡 J cls J S cls J T = J 𝑡 J cls J S cls J T
10 9 eltopss J 𝑡 J cls J S cls J T Top O J 𝑡 J cls J S cls J T O J 𝑡 J cls J S cls J T
11 8 4 10 syl2anc φ O J 𝑡 J cls J S cls J T
12 difssd φ J cls J S cls J T J
13 eqid J = J
14 13 restuni J Top J cls J S cls J T J J cls J S cls J T = J 𝑡 J cls J S cls J T
15 1 12 14 syl2anc φ J cls J S cls J T = J 𝑡 J cls J S cls J T
16 11 15 sseqtrrd φ O J cls J S cls J T
17 1 2 3 16 iscnrm3rlem6 φ O J 𝑡 J cls J S cls J T O J
18 4 17 mpbid φ O J