Metamath Proof Explorer

Theorem en3lpVD

Description: Virtual deduction proof of en3lp . (Contributed by Alan Sare, 24-Oct-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion en3lpVD 
|- -. ( A e. B /\ B e. C /\ C e. A )

Proof

Step Hyp Ref Expression
1 pm2.1 
 |-  ( -. { A , B , C } = (/) \/ { A , B , C } = (/) )
2 df-ne 
 |-  ( { A , B , C } =/= (/) <-> -. { A , B , C } = (/) )
3 2 bicomi 
 |-  ( -. { A , B , C } = (/) <-> { A , B , C } =/= (/) )
4 3 orbi1i 
 |-  ( ( -. { A , B , C } = (/) \/ { A , B , C } = (/) ) <-> ( { A , B , C } =/= (/) \/ { A , B , C } = (/) ) )
5 1 4 mpbi 
 |-  ( { A , B , C } =/= (/) \/ { A , B , C } = (/) )
6 zfregs2 
 |-  ( { A , B , C } =/= (/) -> -. A. x e. { A , B , C } E. y ( y e. { A , B , C } /\ y e. x ) )
7 en3lplem2VD 
 |-  ( ( A e. B /\ B e. C /\ C e. A ) -> ( x e. { A , B , C } -> E. y ( y e. { A , B , C } /\ y e. x ) ) )
8 7 alrimiv 
 |-  ( ( A e. B /\ B e. C /\ C e. A ) -> A. x ( x e. { A , B , C } -> E. y ( y e. { A , B , C } /\ y e. x ) ) )
9 df-ral 
 |-  ( A. x e. { A , B , C } E. y ( y e. { A , B , C } /\ y e. x ) <-> A. x ( x e. { A , B , C } -> E. y ( y e. { A , B , C } /\ y e. x ) ) )
10 8 9 sylibr 
 |-  ( ( A e. B /\ B e. C /\ C e. A ) -> A. x e. { A , B , C } E. y ( y e. { A , B , C } /\ y e. x ) )
11 10 con3i 
 |-  ( -. A. x e. { A , B , C } E. y ( y e. { A , B , C } /\ y e. x ) -> -. ( A e. B /\ B e. C /\ C e. A ) )
12 6 11 syl 
 |-  ( { A , B , C } =/= (/) -> -. ( A e. B /\ B e. C /\ C e. A ) )
13 idn1 
 |-  (. { A , B , C } = (/) ->. { A , B , C } = (/) ).
14 noel 
 |-  -. C e. (/)
15 eleq2 
 |-  ( { A , B , C } = (/) -> ( C e. { A , B , C } <-> C e. (/) ) )
16 15 notbid 
 |-  ( { A , B , C } = (/) -> ( -. C e. { A , B , C } <-> -. C e. (/) ) )
17 16 biimprd 
 |-  ( { A , B , C } = (/) -> ( -. C e. (/) -> -. C e. { A , B , C } ) )
18 13 14 17 e10 
 |-  (. { A , B , C } = (/) ->. -. C e. { A , B , C } ).
19 tpid3g 
 |-  ( C e. A -> C e. { A , B , C } )
20 19 con3i 
 |-  ( -. C e. { A , B , C } -> -. C e. A )
21 18 20 e1a 
 |-  (. { A , B , C } = (/) ->. -. C e. A ).
22 simp3 
 |-  ( ( A e. B /\ B e. C /\ C e. A ) -> C e. A )
23 22 con3i 
 |-  ( -. C e. A -> -. ( A e. B /\ B e. C /\ C e. A ) )
24 21 23 e1a 
 |-  (. { A , B , C } = (/) ->. -. ( A e. B /\ B e. C /\ C e. A ) ).
25 24 in1 
 |-  ( { A , B , C } = (/) -> -. ( A e. B /\ B e. C /\ C e. A ) )
26 12 25 jaoi 
 |-  ( ( { A , B , C } =/= (/) \/ { A , B , C } = (/) ) -> -. ( A e. B /\ B e. C /\ C e. A ) )
27 5 26 ax-mp 
 |-  -. ( A e. B /\ B e. C /\ C e. A )