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 ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ) )