Metamath Proof Explorer

Theorem epne3

Description: A well-founded class contains no 3-cycle loops. (Contributed by NM, 19-Apr-1994) (Revised by Mario Carneiro, 22-Jun-2015)

Ref Expression
Assertion epne3 ⊢ E Fr A ∧ B ∈ A ∧ C ∈ A ∧ D ∈ A → ¬ B ∈ C ∧ C ∈ D ∧ D ∈ B

Proof

Step Hyp Ref Expression
1 fr3nr ⊢ E Fr A ∧ B ∈ A ∧ C ∈ A ∧ D ∈ A → ¬ B E C ∧ C E D ∧ D E B
2 epelg ⊢ C ∈ A → B E C ↔ B ∈ C
3 2 3ad2ant2 ⊢ B ∈ A ∧ C ∈ A ∧ D ∈ A → B E C ↔ B ∈ C
4 epelg ⊢ D ∈ A → C E D ↔ C ∈ D
5 4 3ad2ant3 ⊢ B ∈ A ∧ C ∈ A ∧ D ∈ A → C E D ↔ C ∈ D
6 epelg ⊢ B ∈ A → D E B ↔ D ∈ B
7 6 3ad2ant1 ⊢ B ∈ A ∧ C ∈ A ∧ D ∈ A → D E B ↔ D ∈ B
8 3 5 7 3anbi123d ⊢ B ∈ A ∧ C ∈ A ∧ D ∈ A → B E C ∧ C E D ∧ D E B ↔ B ∈ C ∧ C ∈ D ∧ D ∈ B
9 8 adantl ⊢ E Fr A ∧ B ∈ A ∧ C ∈ A ∧ D ∈ A → B E C ∧ C E D ∧ D E B ↔ B ∈ C ∧ C ∈ D ∧ D ∈ B
10 1 9 mtbid ⊢ E Fr A ∧ B ∈ A ∧ C ∈ A ∧ D ∈ A → ¬ B ∈ C ∧ C ∈ D ∧ D ∈ B