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