This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

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