Metamath Proof Explorer

Theorem iscnrm3rlem7

Description: Lemma for iscnrm3rlem8 . Open neighborhoods in the subspace topology are open neighborhoods in the original topology given that the subspace is an open set in the original topology. (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 )
		iscnrm3rlem7.4	\|- ( ph -> O e. ( J \|`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) )
	Assertion	iscnrm3rlem7	\|- ( ph -> 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		iscnrm3rlem7.4	\|- ( ph -> O e. ( J \|`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) )
5	1	uniexd	\|- ( ph -> U. J e. _V )
6	5	difexd	\|- ( ph -> ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) e. _V )
7		resttop	\|- ( ( J e. Top /\ ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) e. _V ) -> ( J \|`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) e. Top )
8	1 6 7	syl2anc	\|- ( ph -> ( J \|`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) e. Top )
9		eqid	\|- U. ( J \|`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) = U. ( J \|`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) )
10	9	eltopss	\|- ( ( ( J \|`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) e. Top /\ O e. ( J \|`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) -> O C_ U. ( J \|`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) )
11	8 4 10	syl2anc	\|- ( ph -> O C_ U. ( J \|`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) )
12		difssd	\|- ( ph -> ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) C_ U. J )
13		eqid	\|- U. J = U. J
14	13	restuni	\|- ( ( J e. Top /\ ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) C_ U. J ) -> ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) = U. ( J \|`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) )
15	1 12 14	syl2anc	\|- ( ph -> ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) = U. ( J \|`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) )
16	11 15	sseqtrrd	\|- ( ph -> O C_ ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) )
17	1 2 3 16	iscnrm3rlem6	\|- ( ph -> ( O e. ( J \|`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) <-> O e. J ) )
18	4 17	mpbid	\|- ( ph -> O e. J )