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 ⊢EFrA∧B∈A∧C∈A∧D∈A→¬B∈C∧C∈D∧D∈B

Proof

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