Metamath Proof Explorer

Theorem en3lplem2

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

Ref Expression
Assertion en3lplem2 ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → x ∈ A B C → x ∩ A B C ≠ ∅

Proof

Step Hyp Ref Expression
1 en3lplem1 ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → x = A → x ∩ A B C ≠ ∅
2 en3lplem1 ⊢ B ∈ C ∧ C ∈ A ∧ A ∈ B → x = B → x ∩ B C A ≠ ∅
3 2 3comr ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → x = B → x ∩ B C A ≠ ∅
4 3 a1d ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → x ∈ A B C → x = B → x ∩ B C A ≠ ∅
5 tprot ⊢ A B C = B C A
6 5 ineq2i ⊢ x ∩ A B C = x ∩ B C A
7 6 neeq1i ⊢ x ∩ A B C ≠ ∅ ↔ x ∩ B C A ≠ ∅
8 7 bicomi ⊢ x ∩ B C A ≠ ∅ ↔ x ∩ A B C ≠ ∅
9 4 8 syl8ib ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → x ∈ A B C → x = B → x ∩ A B C ≠ ∅
10 jao ⊢ x = A → x ∩ A B C ≠ ∅ → x = B → x ∩ A B C ≠ ∅ → x = A ∨ x = B → x ∩ A B C ≠ ∅
11 1 9 10 sylsyld ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → x ∈ A B C → x = A ∨ x = B → x ∩ A B C ≠ ∅
12 11 imp ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A ∧ x ∈ A B C → x = A ∨ x = B → x ∩ A B C ≠ ∅
13 en3lplem1 ⊢ C ∈ A ∧ A ∈ B ∧ B ∈ C → x = C → x ∩ C A B ≠ ∅
14 13 3coml ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → x = C → x ∩ C A B ≠ ∅
15 14 a1d ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → x ∈ A B C → x = C → x ∩ C A B ≠ ∅
16 tprot ⊢ C A B = A B C
17 16 ineq2i ⊢ x ∩ C A B = x ∩ A B C
18 17 neeq1i ⊢ x ∩ C A B ≠ ∅ ↔ x ∩ A B C ≠ ∅
19 15 18 syl8ib ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → x ∈ A B C → x = C → x ∩ A B C ≠ ∅
20 19 imp ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A ∧ x ∈ A B C → x = C → x ∩ A B C ≠ ∅
21 idd ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → x ∈ A B C → x ∈ A B C
22 dftp2 ⊢ A B C = x | x = A ∨ x = B ∨ x = C
23 22 eleq2i ⊢ x ∈ A B C ↔ x ∈ x | x = A ∨ x = B ∨ x = C
24 21 23 syl6ib ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → x ∈ A B C → x ∈ x | x = A ∨ x = B ∨ x = C
25 abid ⊢ x ∈ x | x = A ∨ x = B ∨ x = C ↔ x = A ∨ x = B ∨ x = C
26 24 25 syl6ib ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → x ∈ 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 ∈ B ∧ B ∈ C ∧ C ∈ A → x ∈ A B C → x = A ∨ x = B ∨ x = C
29 28 imp ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A ∧ x ∈ A B C → x = A ∨ x = B ∨ x = C
30 12 20 29 mpjaod ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A ∧ x ∈ A B C → x ∩ A B C ≠ ∅
31 30 ex ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → x ∈ A B C → x ∩ A B C ≠ ∅