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 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ¬ ( 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐷 ∧ 𝐷 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		fr3nr	⊢ ( ( E Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ¬ ( 𝐵 E 𝐶 ∧ 𝐶 E 𝐷 ∧ 𝐷 E 𝐵 ) )
2		epelg	⊢ ( 𝐶 ∈ 𝐴 → ( 𝐵 E 𝐶 ↔ 𝐵 ∈ 𝐶 ) )
3	2	3ad2ant2	⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) → ( 𝐵 E 𝐶 ↔ 𝐵 ∈ 𝐶 ) )
4		epelg	⊢ ( 𝐷 ∈ 𝐴 → ( 𝐶 E 𝐷 ↔ 𝐶 ∈ 𝐷 ) )
5	4	3ad2ant3	⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) → ( 𝐶 E 𝐷 ↔ 𝐶 ∈ 𝐷 ) )
6		epelg	⊢ ( 𝐵 ∈ 𝐴 → ( 𝐷 E 𝐵 ↔ 𝐷 ∈ 𝐵 ) )
7	6	3ad2ant1	⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) → ( 𝐷 E 𝐵 ↔ 𝐷 ∈ 𝐵 ) )
8	3 5 7	3anbi123d	⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) → ( ( 𝐵 E 𝐶 ∧ 𝐶 E 𝐷 ∧ 𝐷 E 𝐵 ) ↔ ( 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐷 ∧ 𝐷 ∈ 𝐵 ) ) )
9	8	adantl	⊢ ( ( E Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( 𝐵 E 𝐶 ∧ 𝐶 E 𝐷 ∧ 𝐷 E 𝐵 ) ↔ ( 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐷 ∧ 𝐷 ∈ 𝐵 ) ) )
10	1 9	mtbid	⊢ ( ( E Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ¬ ( 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐷 ∧ 𝐷 ∈ 𝐵 ) )