Theorem mapdordlem1bN

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

	Ref	Expression
Hypothesis	mapdordlem1b.c	⊢ 𝐶 = { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) }
Assertion	mapdordlem1bN	⊢ ( 𝐽 ∈ 𝐶 ↔ ( 𝐽 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) = ( 𝐿 ‘ 𝐽 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mapdordlem1b.c	⊢ 𝐶 = { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) }
2	1	lcfl1lem	⊢ ( 𝐽 ∈ 𝐶 ↔ ( 𝐽 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) = ( 𝐿 ‘ 𝐽 ) ) )