Metamath Proof Explorer

Theorem mapdordlem1

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

		Ref	Expression
	Hypothesis	mapdordlem1.t	$⊢ T = \{g \in F \| O (O (L (g))) \in Y\}$
	Assertion	mapdordlem1	$⊢ J \in T \leftrightarrow (J \in F \land O (O (L (J))) \in Y)$

Step	Hyp	Ref	Expression
1		mapdordlem1.t	$⊢ T = \{g \in F \| O (O (L (g))) \in Y\}$
2		2fveq3	$⊢ g = J \to O (L (g)) = O (L (J))$
3	2	fveq2d	$⊢ g = J \to O (O (L (g))) = O (O (L (J)))$
4	3	eleq1d	$⊢ g = J \to (O (O (L (g))) \in Y \leftrightarrow O (O (L (J))) \in Y)$
5	4 1	elrab2	$⊢ J \in T \leftrightarrow (J \in F \land O (O (L (J))) \in Y)$