Metamath Proof Explorer


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 ( ( 𝐴𝐵𝐵𝐶𝐶𝐴 ) → ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } → ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } ) ≠ ∅ ) )