Theorem mapdordlem1

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

	Ref	Expression
Hypothesis	mapdordlem1.t	|- T = { g e. F | ( O ` ( O ` ( L ` g ) ) ) e. Y }
Assertion	mapdordlem1	|- ( J e. T <-> ( J e. F /\ ( O ` ( O ` ( L ` J ) ) ) e. Y ) )

Proof

Step	Hyp	Ref	Expression
1		mapdordlem1.t	|- T = { g e. F | ( O ` ( O ` ( L ` g ) ) ) e. Y }
2		2fveq3	|- ( g = J -> ( O ` ( L ` g ) ) = ( O ` ( L ` J ) ) )
3	2	fveq2d	|- ( g = J -> ( O ` ( O ` ( L ` g ) ) ) = ( O ` ( O ` ( L ` J ) ) ) )
4	3	eleq1d	|- ( g = J -> ( ( O ` ( O ` ( L ` g ) ) ) e. Y <-> ( O ` ( O ` ( L ` J ) ) ) e. Y ) )
5	4 1	elrab2	|- ( J e. T <-> ( J e. F /\ ( O ` ( O ` ( L ` J ) ) ) e. Y ) )