Metamath Proof Explorer

Theorem mapdordlem1

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

Ref Expression
Hypothesis mapdordlem1.t ⊢ T = g ∈ F | O ⁡ O ⁡ L ⁡ g ∈ Y
Assertion mapdordlem1 ⊢ J ∈ T ↔ J ∈ F ∧ O ⁡ O ⁡ L ⁡ J ∈ Y

Proof

Step Hyp Ref Expression
1 mapdordlem1.t ⊢ T = g ∈ F | O ⁡ O ⁡ L ⁡ g ∈ 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 ∈ Y ↔ O ⁡ O ⁡ L ⁡ J ∈ Y
5 4 1 elrab2 ⊢ J ∈ T ↔ J ∈ F ∧ O ⁡ O ⁡ L ⁡ J ∈ Y