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