Theorem mapdordlem1

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

	Ref	Expression
Hypothesis	mapdordlem1.t	⊢ 𝑇 = { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) ∈ 𝑌 }
Assertion	mapdordlem1	⊢ ( 𝐽 ∈ 𝑇 ↔ ( 𝐽 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) ∈ 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		mapdordlem1.t	⊢ 𝑇 = { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) ∈ 𝑌 }
2		2fveq3	⊢ ( 𝑔 = 𝐽 → ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) = ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) )
3	2	fveq2d	⊢ ( 𝑔 = 𝐽 → ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) )
4	3	eleq1d	⊢ ( 𝑔 = 𝐽 → ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) ∈ 𝑌 ↔ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) ∈ 𝑌 ) )
5	4 1	elrab2	⊢ ( 𝐽 ∈ 𝑇 ↔ ( 𝐽 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) ∈ 𝑌 ) )