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

Metamath Proof Explorer

Theorem lhpexle3

Description: There exists atom under a co-atom different from any three other elements. (Contributed by NM, 24-Jul-2013)

Ref Expression
Hypotheses lhpex1.l ⊢ ≤ = ( le ‘ 𝐾 )
lhpex1.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lhpex1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion lhpexle3 ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 lhpex1.l ⊢ ≤ = ( le ‘ 𝐾 )
2 lhpex1.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3 lhpex1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 1 2 3 lhpexle2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ) )
5 3anass ⊢ ( ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ) ↔ ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ) ) )
6 5 rexbii ⊢ ( ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ) ↔ ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ) ) )
7 4 6 sylib ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ) ) )
8 1 2 3 lhpexle2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) )
9 8 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊 ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) )
10 3anass ⊢ ( ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) ↔ ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) ) )
11 10 rexbii ⊢ ( ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) ↔ ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) ) )
12 9 11 sylib ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊 ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) ) )
13 1 2 3 lhpexle2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) )
14 3anass ⊢ ( ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ↔ ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ) )
15 14 rexbii ⊢ ( ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ↔ ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ) )
16 13 15 sylib ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ) )
17 16 3ad2ant1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ) )
18 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
19 simpl3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) → 𝑌 ∈ 𝐴 )
20 simpl2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) → 𝑍 ∈ 𝐴 )
21 simprl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) → 𝑋 ∈ 𝐴 )
22 simpl3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) → 𝑌 ≤ 𝑊 )
23 simpl2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) → 𝑍 ≤ 𝑊 )
24 simprr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) → 𝑋 ≤ 𝑊 )
25 1 2 3 lhpexle3lem ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ∧ 𝑋 ≤ 𝑊 ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ∧ 𝑝 ≠ 𝑋 ) ) )
26 18 19 20 21 22 23 24 25 syl133anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ∧ 𝑝 ≠ 𝑋 ) ) )
27 df-3an ⊢ ( ( 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ∧ 𝑝 ≠ 𝑋 ) ↔ ( ( 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ∧ 𝑝 ≠ 𝑋 ) )
28 27 anbi2i ⊢ ( ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ∧ 𝑝 ≠ 𝑋 ) ) ↔ ( 𝑝 ≤ 𝑊 ∧ ( ( 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ∧ 𝑝 ≠ 𝑋 ) ) )
29 3anass ⊢ ( ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ∧ 𝑝 ≠ 𝑋 ) ↔ ( 𝑝 ≤ 𝑊 ∧ ( ( 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ∧ 𝑝 ≠ 𝑋 ) ) )
30 28 29 bitr4i ⊢ ( ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ∧ 𝑝 ≠ 𝑋 ) ) ↔ ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ∧ 𝑝 ≠ 𝑋 ) )
31 30 rexbii ⊢ ( ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ∧ 𝑝 ≠ 𝑋 ) ) ↔ ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ∧ 𝑝 ≠ 𝑋 ) )
32 26 31 sylib ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ∧ 𝑝 ≠ 𝑋 ) )
33 17 32 lhpexle1lem ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ∧ 𝑝 ≠ 𝑋 ) )
34 an31 ⊢ ( ( ( 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ∧ 𝑝 ≠ 𝑋 ) ↔ ( ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) ∧ 𝑝 ≠ 𝑌 ) )
35 34 anbi2i ⊢ ( ( 𝑝 ≤ 𝑊 ∧ ( ( 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ∧ 𝑝 ≠ 𝑋 ) ) ↔ ( 𝑝 ≤ 𝑊 ∧ ( ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) ∧ 𝑝 ≠ 𝑌 ) ) )
36 3anass ⊢ ( ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) ∧ 𝑝 ≠ 𝑌 ) ↔ ( 𝑝 ≤ 𝑊 ∧ ( ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) ∧ 𝑝 ≠ 𝑌 ) ) )
37 35 29 36 3bitr4i ⊢ ( ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ∧ 𝑝 ≠ 𝑋 ) ↔ ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) ∧ 𝑝 ≠ 𝑌 ) )
38 37 rexbii ⊢ ( ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ∧ 𝑝 ≠ 𝑋 ) ↔ ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) ∧ 𝑝 ≠ 𝑌 ) )
39 33 38 sylib ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) ∧ 𝑝 ≠ 𝑌 ) )
40 39 3expa ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊 ) ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) ∧ 𝑝 ≠ 𝑌 ) )
41 12 40 lhpexle1lem ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊 ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) ∧ 𝑝 ≠ 𝑌 ) )
42 an32 ⊢ ( ( ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) ∧ 𝑝 ≠ 𝑌 ) ↔ ( ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ) ∧ 𝑝 ≠ 𝑍 ) )
43 42 anbi2i ⊢ ( ( 𝑝 ≤ 𝑊 ∧ ( ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) ∧ 𝑝 ≠ 𝑌 ) ) ↔ ( 𝑝 ≤ 𝑊 ∧ ( ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ) ∧ 𝑝 ≠ 𝑍 ) ) )
44 3anass ⊢ ( ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ) ∧ 𝑝 ≠ 𝑍 ) ↔ ( 𝑝 ≤ 𝑊 ∧ ( ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ) ∧ 𝑝 ≠ 𝑍 ) ) )
45 43 36 44 3bitr4i ⊢ ( ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) ∧ 𝑝 ≠ 𝑌 ) ↔ ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ) ∧ 𝑝 ≠ 𝑍 ) )
46 45 rexbii ⊢ ( ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) ∧ 𝑝 ≠ 𝑌 ) ↔ ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ) ∧ 𝑝 ≠ 𝑍 ) )
47 41 46 sylib ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊 ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ) ∧ 𝑝 ≠ 𝑍 ) )
48 7 47 lhpexle1lem ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ) ∧ 𝑝 ≠ 𝑍 ) )
49 df-3an ⊢ ( ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ↔ ( ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ) ∧ 𝑝 ≠ 𝑍 ) )
50 49 anbi2i ⊢ ( ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ) ↔ ( 𝑝 ≤ 𝑊 ∧ ( ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ) ∧ 𝑝 ≠ 𝑍 ) ) )
51 44 50 bitr4i ⊢ ( ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ) ∧ 𝑝 ≠ 𝑍 ) ↔ ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ) )
52 51 rexbii ⊢ ( ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ) ∧ 𝑝 ≠ 𝑍 ) ↔ ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ) )
53 48 52 sylib ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ) )