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 imbitrdi 
 |-  ( ( 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 imbitrdi 
 |-  ( ( 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 imbitrdi 
 |-  ( ( 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 } ) =/= (/) ) )