Theorem mapdordlem1bN

Description: Lemma for mapdord . (Contributed by NM, 27-Jan-2015) (New usage is discouraged.)

	Ref	Expression
Hypothesis	mapdordlem1b.c	|- C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }
Assertion	mapdordlem1bN	|- ( J e. C <-> ( J e. F /\ ( O ` ( O ` ( L ` J ) ) ) = ( L ` J ) ) )

Proof

Step	Hyp	Ref	Expression
1		mapdordlem1b.c	|- C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }
2	1	lcfl1lem	|- ( J e. C <-> ( J e. F /\ ( O ` ( O ` ( L ` J ) ) ) = ( L ` J ) ) )