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