Theorem en3lplem2

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

	Ref	Expression
Assertion	en3lplem2	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } → ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } ) ≠ ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		en3lplem1	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑥 = 𝐴 → ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } ) ≠ ∅ ) )
2		en3lplem1	⊢ ( ( 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ) → ( 𝑥 = 𝐵 → ( 𝑥 ∩ { 𝐵 , 𝐶 , 𝐴 } ) ≠ ∅ ) )
3	2	3comr	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑥 = 𝐵 → ( 𝑥 ∩ { 𝐵 , 𝐶 , 𝐴 } ) ≠ ∅ ) )
4	3	a1d	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } → ( 𝑥 = 𝐵 → ( 𝑥 ∩ { 𝐵 , 𝐶 , 𝐴 } ) ≠ ∅ ) ) )
5		tprot	⊢ { 𝐴 , 𝐵 , 𝐶 } = { 𝐵 , 𝐶 , 𝐴 }
6	5	ineq2i	⊢ ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } ) = ( 𝑥 ∩ { 𝐵 , 𝐶 , 𝐴 } )
7	6	neeq1i	⊢ ( ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } ) ≠ ∅ ↔ ( 𝑥 ∩ { 𝐵 , 𝐶 , 𝐴 } ) ≠ ∅ )
8	7	bicomi	⊢ ( ( 𝑥 ∩ { 𝐵 , 𝐶 , 𝐴 } ) ≠ ∅ ↔ ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } ) ≠ ∅ )
9	4 8	syl8ib	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } → ( 𝑥 = 𝐵 → ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } ) ≠ ∅ ) ) )
10		jao	⊢ ( ( 𝑥 = 𝐴 → ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } ) ≠ ∅ ) → ( ( 𝑥 = 𝐵 → ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } ) ≠ ∅ ) → ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } ) ≠ ∅ ) ) )
11	1 9 10	sylsyld	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } → ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } ) ≠ ∅ ) ) )
12	11	imp	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) ∧ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ) → ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } ) ≠ ∅ ) )
13		en3lplem1	⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ) → ( 𝑥 = 𝐶 → ( 𝑥 ∩ { 𝐶 , 𝐴 , 𝐵 } ) ≠ ∅ ) )
14	13	3coml	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑥 = 𝐶 → ( 𝑥 ∩ { 𝐶 , 𝐴 , 𝐵 } ) ≠ ∅ ) )
15	14	a1d	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } → ( 𝑥 = 𝐶 → ( 𝑥 ∩ { 𝐶 , 𝐴 , 𝐵 } ) ≠ ∅ ) ) )
16		tprot	⊢ { 𝐶 , 𝐴 , 𝐵 } = { 𝐴 , 𝐵 , 𝐶 }
17	16	ineq2i	⊢ ( 𝑥 ∩ { 𝐶 , 𝐴 , 𝐵 } ) = ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } )
18	17	neeq1i	⊢ ( ( 𝑥 ∩ { 𝐶 , 𝐴 , 𝐵 } ) ≠ ∅ ↔ ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } ) ≠ ∅ )
19	15 18	syl8ib	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } → ( 𝑥 = 𝐶 → ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } ) ≠ ∅ ) ) )
20	19	imp	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) ∧ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ) → ( 𝑥 = 𝐶 → ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } ) ≠ ∅ ) )
21		idd	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } → 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ) )
22		dftp2	⊢ { 𝐴 , 𝐵 , 𝐶 } = { 𝑥 ∣ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ) }
23	22	eleq2i	⊢ ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ↔ 𝑥 ∈ { 𝑥 ∣ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ) } )
24	21 23	syl6ib	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } → 𝑥 ∈ { 𝑥 ∣ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ) } ) )
25		abid	⊢ ( 𝑥 ∈ { 𝑥 ∣ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ) } ↔ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ) )
26	24 25	syl6ib	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } → ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ) ) )
27		df-3or	⊢ ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ) ↔ ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ∨ 𝑥 = 𝐶 ) )
28	26 27	syl6ib	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } → ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ∨ 𝑥 = 𝐶 ) ) )
29	28	imp	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) ∧ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ) → ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ∨ 𝑥 = 𝐶 ) )
30	12 20 29	mpjaod	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) ∧ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ) → ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } ) ≠ ∅ )
31	30	ex	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } → ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } ) ≠ ∅ ) )