Metamath Proof Explorer


Theorem en3lplem2

Description: Lemma for en3lp . (Contributed by Alan Sare, 28-Oct-2011)

Ref Expression
Assertion en3lplem2
|- ( ( A e. B /\ B e. C /\ C e. A ) -> ( x e. { A , B , C } -> ( x i^i { A , B , C } ) =/= (/) ) )

Proof

Step Hyp Ref Expression
1 en3lplem1
 |-  ( ( A e. B /\ B e. C /\ C e. A ) -> ( x = A -> ( x i^i { A , B , C } ) =/= (/) ) )
2 en3lplem1
 |-  ( ( B e. C /\ C e. A /\ A e. B ) -> ( x = B -> ( x i^i { B , C , A } ) =/= (/) ) )
3 2 3comr
 |-  ( ( A e. B /\ B e. C /\ C e. A ) -> ( x = B -> ( x i^i { B , C , A } ) =/= (/) ) )
4 3 a1d
 |-  ( ( A e. B /\ B e. C /\ C e. A ) -> ( x e. { A , B , C } -> ( x = B -> ( x i^i { B , C , A } ) =/= (/) ) ) )
5 tprot
 |-  { A , B , C } = { B , C , A }
6 5 ineq2i
 |-  ( x i^i { A , B , C } ) = ( x i^i { B , C , A } )
7 6 neeq1i
 |-  ( ( x i^i { A , B , C } ) =/= (/) <-> ( x i^i { B , C , A } ) =/= (/) )
8 7 bicomi
 |-  ( ( x i^i { B , C , A } ) =/= (/) <-> ( x i^i { A , B , C } ) =/= (/) )
9 4 8 syl8ib
 |-  ( ( A e. B /\ B e. C /\ C e. A ) -> ( x e. { A , B , C } -> ( x = B -> ( x i^i { A , B , C } ) =/= (/) ) ) )
10 jao
 |-  ( ( x = A -> ( x i^i { A , B , C } ) =/= (/) ) -> ( ( x = B -> ( x i^i { A , B , C } ) =/= (/) ) -> ( ( x = A \/ x = B ) -> ( x i^i { A , B , C } ) =/= (/) ) ) )
11 1 9 10 sylsyld
 |-  ( ( A e. B /\ B e. C /\ C e. A ) -> ( x e. { A , B , C } -> ( ( x = A \/ x = B ) -> ( x i^i { A , B , C } ) =/= (/) ) ) )
12 11 imp
 |-  ( ( ( A e. B /\ B e. C /\ C e. A ) /\ x e. { A , B , C } ) -> ( ( x = A \/ x = B ) -> ( x i^i { A , B , C } ) =/= (/) ) )
13 en3lplem1
 |-  ( ( C e. A /\ A e. B /\ B e. C ) -> ( x = C -> ( x i^i { C , A , B } ) =/= (/) ) )
14 13 3coml
 |-  ( ( A e. B /\ B e. C /\ C e. A ) -> ( x = C -> ( x i^i { C , A , B } ) =/= (/) ) )
15 14 a1d
 |-  ( ( A e. B /\ B e. C /\ C e. A ) -> ( x e. { A , B , C } -> ( x = C -> ( x i^i { C , A , B } ) =/= (/) ) ) )
16 tprot
 |-  { C , A , B } = { A , B , C }
17 16 ineq2i
 |-  ( x i^i { C , A , B } ) = ( x i^i { A , B , C } )
18 17 neeq1i
 |-  ( ( x i^i { C , A , B } ) =/= (/) <-> ( x i^i { A , B , C } ) =/= (/) )
19 15 18 syl8ib
 |-  ( ( A e. B /\ B e. C /\ C e. A ) -> ( x e. { A , B , C } -> ( x = C -> ( x i^i { A , B , C } ) =/= (/) ) ) )
20 19 imp
 |-  ( ( ( A e. B /\ B e. C /\ C e. A ) /\ x e. { A , B , C } ) -> ( x = C -> ( x i^i { A , B , C } ) =/= (/) ) )
21 idd
 |-  ( ( A e. B /\ B e. C /\ C e. A ) -> ( x e. { A , B , C } -> x e. { A , B , C } ) )
22 dftp2
 |-  { A , B , C } = { x | ( x = A \/ x = B \/ x = C ) }
23 22 eleq2i
 |-  ( x e. { A , B , C } <-> x e. { x | ( x = A \/ x = B \/ x = C ) } )
24 21 23 syl6ib
 |-  ( ( A e. B /\ B e. C /\ C e. A ) -> ( x e. { A , B , C } -> x e. { x | ( x = A \/ x = B \/ x = C ) } ) )
25 abid
 |-  ( x e. { x | ( x = A \/ x = B \/ x = C ) } <-> ( x = A \/ x = B \/ x = C ) )
26 24 25 syl6ib
 |-  ( ( A e. B /\ B e. C /\ C e. A ) -> ( x e. { A , B , C } -> ( x = A \/ x = B \/ x = C ) ) )
27 df-3or
 |-  ( ( x = A \/ x = B \/ x = C ) <-> ( ( x = A \/ x = B ) \/ x = C ) )
28 26 27 syl6ib
 |-  ( ( A e. B /\ B e. C /\ C e. A ) -> ( x e. { A , B , C } -> ( ( x = A \/ x = B ) \/ x = C ) ) )
29 28 imp
 |-  ( ( ( A e. B /\ B e. C /\ C e. A ) /\ x e. { A , B , C } ) -> ( ( x = A \/ x = B ) \/ x = C ) )
30 12 20 29 mpjaod
 |-  ( ( ( A e. B /\ B e. C /\ C e. A ) /\ x e. { A , B , C } ) -> ( x i^i { A , B , C } ) =/= (/) )
31 30 ex
 |-  ( ( A e. B /\ B e. C /\ C e. A ) -> ( x e. { A , B , C } -> ( x i^i { A , B , C } ) =/= (/) ) )