Metamath Proof Explorer


Theorem iscnrm3rlem5

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

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

Proof

Step Hyp Ref Expression
1 iscnrm3rlem4.1 φ J Top
2 iscnrm3rlem4.2 φ S J
3 iscnrm3rlem5.3 φ T J
4 eqid J = J
5 4 clscld J Top S J cls J S Clsd J
6 1 2 5 syl2anc φ cls J S Clsd J
7 4 clscld J Top T J cls J T Clsd J
8 1 3 7 syl2anc φ cls J T Clsd J
9 incld cls J S Clsd J cls J T Clsd J cls J S cls J T Clsd J
10 6 8 9 syl2anc φ cls J S cls J T Clsd J
11 4 cldopn cls J S cls J T Clsd J J cls J S cls J T J
12 10 11 syl φ J cls J S cls J T J