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 e. B /\ B e. C /\ C e. A )

Proof

Step Hyp Ref Expression
1 noel 
 |-  -. C e. (/)
2 eleq2 
 |-  ( { A , B , C } = (/) -> ( C e. { A , B , C } <-> C e. (/) ) )
3 1 2 mtbiri 
 |-  ( { A , B , C } = (/) -> -. C e. { A , B , C } )
4 tpid3g 
 |-  ( C e. A -> C e. { A , B , C } )
5 3 4 nsyl 
 |-  ( { A , B , C } = (/) -> -. C e. A )
6 5 intn3an3d 
 |-  ( { A , B , C } = (/) -> -. ( A e. B /\ B e. C /\ C e. A ) )
7 tpex 
 |-  { A , B , C } e. _V
8 zfreg 
 |-  ( ( { A , B , C } e. _V /\ { A , B , C } =/= (/) ) -> E. x e. { A , B , C } ( x i^i { A , B , C } ) = (/) )
9 7 8 mpan 
 |-  ( { A , B , C } =/= (/) -> E. x e. { A , B , C } ( x i^i { A , B , C } ) = (/) )
10 en3lplem2 
 |-  ( ( A e. B /\ B e. C /\ C e. A ) -> ( x e. { A , B , C } -> ( x i^i { A , B , C } ) =/= (/) ) )
11 10 com12 
 |-  ( x e. { A , B , C } -> ( ( A e. B /\ B e. C /\ C e. A ) -> ( x i^i { A , B , C } ) =/= (/) ) )
12 11 necon2bd 
 |-  ( x e. { A , B , C } -> ( ( x i^i { A , B , C } ) = (/) -> -. ( A e. B /\ B e. C /\ C e. A ) ) )
13 12 rexlimiv 
 |-  ( E. x e. { A , B , C } ( x i^i { A , B , C } ) = (/) -> -. ( A e. B /\ B e. C /\ C e. A ) )
14 9 13 syl 
 |-  ( { A , B , C } =/= (/) -> -. ( A e. B /\ B e. C /\ C e. A ) )
15 6 14 pm2.61ine 
 |-  -. ( A e. B /\ B e. C /\ C e. A )