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 ⊢ABC=∅→C∈ABC↔C∈∅
3 1 2 mtbiri ⊢ABC=∅→¬C∈ABC
4 tpid3g ⊢C∈A→C∈ABC
5 3 4 nsyl ⊢ABC=∅→¬C∈A
6 5 intn3an3d ⊢ABC=∅→¬A∈B∧B∈C∧C∈A
7 tpex ⊢ABC∈V
8 zfreg ⊢ABC∈V∧ABC≠∅→∃x∈ABCx∩ABC=∅
9 7 8 mpan ⊢ABC≠∅→∃x∈ABCx∩ABC=∅
10 en3lplem2 ⊢A∈B∧B∈C∧C∈A→x∈ABC→x∩ABC≠∅
11 10 com12 ⊢x∈ABC→A∈B∧B∈C∧C∈A→x∩ABC≠∅
12 11 necon2bd ⊢x∈ABC→x∩ABC=∅→¬A∈B∧B∈C∧C∈A
13 12 rexlimiv ⊢∃x∈ABCx∩ABC=∅→¬A∈B∧B∈C∧C∈A
14 9 13 syl ⊢ABC≠∅→¬A∈B∧B∈C∧C∈A
15 6 14 pm2.61ine ⊢¬A∈B∧B∈C∧C∈A