Theorem iscnrm3rlem5

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

	Ref	Expression
Hypotheses	iscnrm3rlem4.1	|- ( ph -> J e. Top )
	iscnrm3rlem4.2	|- ( ph -> S C_ U. J )
	iscnrm3rlem5.3	|- ( ph -> T C_ U. J )
Assertion	iscnrm3rlem5	|- ( ph -> ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) e. J )

Proof

Step	Hyp	Ref	Expression
1		iscnrm3rlem4.1	|- ( ph -> J e. Top )
2		iscnrm3rlem4.2	|- ( ph -> S C_ U. J )
3		iscnrm3rlem5.3	|- ( ph -> T C_ U. J )
4		eqid	|- U. J = U. J
5	4	clscld	|- ( ( J e. Top /\ S C_ U. J ) -> ( ( cls ` J ) ` S ) e. ( Clsd ` J ) )
6	1 2 5	syl2anc	|- ( ph -> ( ( cls ` J ) ` S ) e. ( Clsd ` J ) )
7	4	clscld	|- ( ( J e. Top /\ T C_ U. J ) -> ( ( cls ` J ) ` T ) e. ( Clsd ` J ) )
8	1 3 7	syl2anc	|- ( ph -> ( ( cls ` J ) ` T ) e. ( Clsd ` J ) )
9		incld	|- ( ( ( ( cls ` J ) ` S ) e. ( Clsd ` J ) /\ ( ( cls ` J ) ` T ) e. ( Clsd ` J ) ) -> ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) e. ( Clsd ` J ) )
10	6 8 9	syl2anc	|- ( ph -> ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) e. ( Clsd ` J ) )
11	4	cldopn	|- ( ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) e. ( Clsd ` J ) -> ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) e. J )
12	10 11	syl	|- ( ph -> ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) e. J )