Metamath Proof Explorer

Theorem iscnrm3rlem2

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

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

Proof

Step	Hyp	Ref	Expression
1		iscnrm3rlem2.1	\|- ( ph -> J e. Top )
2		iscnrm3rlem2.2	\|- ( ph -> S C_ U. J )
3		eqid	\|- U. J = U. J
4	3	clscld	\|- ( ( J e. Top /\ S C_ U. J ) -> ( ( cls ` J ) ` S ) e. ( Clsd ` J ) )
5	3	clsss3	\|- ( ( J e. Top /\ S C_ U. J ) -> ( ( cls ` J ) ` S ) C_ U. J )
6	5	iscnrm3rlem1	\|- ( ( J e. Top /\ S C_ U. J ) -> ( ( ( cls ` J ) ` S ) \ T ) = ( ( ( cls ` J ) ` S ) i^i ( U. J \ ( ( ( cls ` J ) ` S ) i^i T ) ) ) )
7		ineq1	\|- ( c = ( ( cls ` J ) ` S ) -> ( c i^i ( U. J \ ( ( ( cls ` J ) ` S ) i^i T ) ) ) = ( ( ( cls ` J ) ` S ) i^i ( U. J \ ( ( ( cls ` J ) ` S ) i^i T ) ) ) )
8	7	rspceeqv	\|- ( ( ( ( cls ` J ) ` S ) e. ( Clsd ` J ) /\ ( ( ( cls ` J ) ` S ) \ T ) = ( ( ( cls ` J ) ` S ) i^i ( U. J \ ( ( ( cls ` J ) ` S ) i^i T ) ) ) ) -> E. c e. ( Clsd ` J ) ( ( ( cls ` J ) ` S ) \ T ) = ( c i^i ( U. J \ ( ( ( cls ` J ) ` S ) i^i T ) ) ) )
9	4 6 8	syl2anc	\|- ( ( J e. Top /\ S C_ U. J ) -> E. c e. ( Clsd ` J ) ( ( ( cls ` J ) ` S ) \ T ) = ( c i^i ( U. J \ ( ( ( cls ` J ) ` S ) i^i T ) ) ) )
10	1 2 9	syl2anc	\|- ( ph -> E. c e. ( Clsd ` J ) ( ( ( cls ` J ) ` S ) \ T ) = ( c i^i ( U. J \ ( ( ( cls ` J ) ` S ) i^i T ) ) ) )
11		difss	\|- ( U. J \ ( ( ( cls ` J ) ` S ) i^i T ) ) C_ U. J
12	3	restcld	\|- ( ( J e. Top /\ ( U. J \ ( ( ( cls ` J ) ` S ) i^i T ) ) C_ U. J ) -> ( ( ( ( cls ` J ) ` S ) \ T ) e. ( Clsd ` ( J \|`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i T ) ) ) ) <-> E. c e. ( Clsd ` J ) ( ( ( cls ` J ) ` S ) \ T ) = ( c i^i ( U. J \ ( ( ( cls ` J ) ` S ) i^i T ) ) ) ) )
13	1 11 12	sylancl	\|- ( ph -> ( ( ( ( cls ` J ) ` S ) \ T ) e. ( Clsd ` ( J \|`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i T ) ) ) ) <-> E. c e. ( Clsd ` J ) ( ( ( cls ` J ) ` S ) \ T ) = ( c i^i ( U. J \ ( ( ( cls ` J ) ` S ) i^i T ) ) ) ) )
14	10 13	mpbird	\|- ( ph -> ( ( ( cls ` J ) ` S ) \ T ) e. ( Clsd ` ( J \|`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i T ) ) ) ) )