Metamath Proof Explorer


Theorem iscnrm3rlem6

Description: Lemma for iscnrm3rlem7 . (Contributed by Zhi Wang, 5-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 iscnrm3rlem4.1 φ J Top
2 iscnrm3rlem4.2 φ S J
3 iscnrm3rlem5.3 φ T J
4 iscnrm3rlem6.4 φ O J cls J S cls J T
5 1 2 3 iscnrm3rlem5 φ J cls J S cls J T J
6 restopn2 J Top J cls J S cls J T J O J 𝑡 J cls J S cls J T O J O J cls J S cls J T
7 1 5 6 syl2anc φ O J 𝑡 J cls J S cls J T O J O J cls J S cls J T
8 4 7 mpbiran2d φ O J 𝑡 J cls J S cls J T O J