Theorem iscnrm3rlem6

Description: Lemma for iscnrm3rlem7 . (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 )
	iscnrm3rlem6.4	|- ( ph -> O C_ ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) )
Assertion	iscnrm3rlem6	|- ( ph -> ( O e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) <-> O 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		iscnrm3rlem6.4	|- ( ph -> O C_ ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) )
5	1 2 3	iscnrm3rlem5	|- ( ph -> ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) e. J )
6		restopn2	|- ( ( J e. Top /\ ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) e. J ) -> ( O e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) <-> ( O e. J /\ O C_ ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) )
7	1 5 6	syl2anc	|- ( ph -> ( O e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) <-> ( O e. J /\ O C_ ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) )
8	4 7	mpbiran2d	|- ( ph -> ( O e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) <-> O e. J ) )