Metamath Proof Explorer

Theorem iscnrm3lem1

Description: Lemma for iscnrm3 . Subspace topology is a topology. (Contributed by Zhi Wang, 3-Sep-2024)

		Ref	Expression
	Assertion	iscnrm3lem1	\|- ( J e. Top -> ( A. x e. A ph <-> A. x e. A ( ( J \|`t x ) e. Top /\ ph ) ) )

Step	Hyp	Ref	Expression
1		resttop	\|- ( ( J e. Top /\ x e. A ) -> ( J \|`t x ) e. Top )
2	1	biantrurd	\|- ( ( J e. Top /\ x e. A ) -> ( ph <-> ( ( J \|`t x ) e. Top /\ ph ) ) )
3	2	ralbidva	\|- ( J e. Top -> ( A. x e. A ph <-> A. x e. A ( ( J \|`t x ) e. Top /\ ph ) ) )

Step

Hyp

Ref

Expression

 |-  ( ( J e. Top /\ x e. A ) -> ( J |`t x ) e. Top )

 |-  ( ( J e. Top /\ x e. A ) -> ( ph <-> ( ( J |`t x ) e. Top /\ ph ) ) )

 |-  ( J e. Top -> ( A. x e. A ph <-> A. x e. A ( ( J |`t x ) e. Top /\ ph ) ) )