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∈ABC→x∩ABC≠∅

Proof

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