Theorem mapdordlem1bN

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

	Ref	Expression
Hypothesis	mapdordlem1b.c	$$⊢C=\left\{g\in F|O\left(O\left(L\left(g\right)\right)\right)=L\left(g\right)\right\}$$
Assertion	mapdordlem1bN	$$⊢J\in C\leftrightarrow \left(J\in F\wedge O\left(O\left(L\left(J\right)\right)\right)=L\left(J\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mapdordlem1b.c	$$⊢C=\left\{g\in F|O\left(O\left(L\left(g\right)\right)\right)=L\left(g\right)\right\}$$
2	1	lcfl1lem	$$⊢J\in C\leftrightarrow \left(J\in F\wedge O\left(O\left(L\left(J\right)\right)\right)=L\left(J\right)\right)$$