This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrdi ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } → 𝑥 ∈ { 𝑥 ∣ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ) } ) )
25 abid ⊢ ( 𝑥 ∈ { 𝑥 ∣ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ) } ↔ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ) )
26 24 25 imbitrdi ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } → ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ) ) )
27 df-3or ⊢ ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ) ↔ ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ∨ 𝑥 = 𝐶 ) )
28 26 27 imbitrdi ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } → ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ∨ 𝑥 = 𝐶 ) ) )
29 28 imp ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) ∧ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ) → ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ∨ 𝑥 = 𝐶 ) )
30 12 20 29 mpjaod ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) ∧ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ) → ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } ) ≠ ∅ )
31 30 ex ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } → ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } ) ≠ ∅ ) )