Metamath Proof Explorer

Theorem en3lp

Description: No class has 3-cycle membership loops. This proof was automatically generated from the virtual deduction proof en3lpVD using a translation program. (Contributed by Alan Sare, 24-Oct-2011)

Ref Expression
Assertion en3lp ⊢ ¬ A ∈ B ∧ B ∈ C ∧ C ∈ A

Proof

Step Hyp Ref Expression
1 noel ⊢ ¬ C ∈ ∅
2 eleq2 ⊢ A B C = ∅ → C ∈ A B C ↔ C ∈ ∅
3 1 2 mtbiri ⊢ A B C = ∅ → ¬ C ∈ A B C
4 tpid3g ⊢ C ∈ A → C ∈ A B C
5 3 4 nsyl ⊢ A B C = ∅ → ¬ C ∈ A
6 5 intn3an3d ⊢ A B C = ∅ → ¬ A ∈ B ∧ B ∈ C ∧ C ∈ A
7 tpex ⊢ A B C ∈ V
8 zfreg ⊢ A B C ∈ V ∧ A B C ≠ ∅ → ∃ x ∈ A B C x ∩ A B C = ∅
9 7 8 mpan ⊢ A B C ≠ ∅ → ∃ x ∈ A B C x ∩ A B C = ∅
10 en3lplem2 ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → x ∈ A B C → x ∩ A B C ≠ ∅
11 10 com12 ⊢ x ∈ A B C → A ∈ B ∧ B ∈ C ∧ C ∈ A → x ∩ A B C ≠ ∅
12 11 necon2bd ⊢ x ∈ A B C → x ∩ A B C = ∅ → ¬ A ∈ B ∧ B ∈ C ∧ C ∈ A
13 12 rexlimiv ⊢ ∃ x ∈ A B C x ∩ A B C = ∅ → ¬ A ∈ B ∧ B ∈ C ∧ C ∈ A
14 9 13 syl ⊢ A B C ≠ ∅ → ¬ A ∈ B ∧ B ∈ C ∧ C ∈ A
15 6 14 pm2.61ine ⊢ ¬ A ∈ B ∧ B ∈ C ∧ C ∈ A