Theorem lcfl1lem

Description: Property of a functional with a closed kernel. (Contributed by NM, 28-Dec-2014)

	Ref	Expression
Hypothesis	lcfl1.c	|- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
Assertion	lcfl1lem	|- ( G e. C <-> ( G e. F /\ ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) ) )

Proof

Step	Hyp	Ref	Expression
1		lcfl1.c	|- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
2		fveq2	|- ( f = G -> ( L ` f ) = ( L ` G ) )
3	2	fveq2d	|- ( f = G -> ( ._|_ ` ( L ` f ) ) = ( ._|_ ` ( L ` G ) ) )
4	3	fveq2d	|- ( f = G -> ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) )
5	4 2	eqeq12d	|- ( f = G -> ( ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) <-> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) ) )
6	5 1	elrab2	|- ( G e. C <-> ( G e. F /\ ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) ) )