Theorem cdleme0nex

Description: Part of proof of Lemma E in Crawley p. 114, 4th line of 4th paragraph. Whenever (in their terminology) p \/ q/0 (i.e. the sublattice from 0 to p \/ q) contains precisely three atoms, any atom not under w must equal either p or q. (In case of 3 atoms, one of them must be u - see cdleme0a - which is under w, so the only 2 left not under w are p and q themselves.) Note that by cvlsupr2 , our ( P .\/ r ) = ( Q .\/ r ) is a shorter way to express r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) . Thus, the negated existential condition states there are no atoms different from p or q that are also not under w. (Contributed by NM, 12-Nov-2012)

	Ref	Expression
Hypotheses	cdleme0nex.l	⊢ ≤ = ( le ‘ 𝐾 )
	cdleme0nex.j	⊢ ∨ = ( join ‘ 𝐾 )
	cdleme0nex.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	cdleme0nex	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( 𝑅 = 𝑃 ∨ 𝑅 = 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		cdleme0nex.l	⊢ ≤ = ( le ‘ 𝐾 )
2		cdleme0nex.j	⊢ ∨ = ( join ‘ 𝐾 )
3		cdleme0nex.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		simp3r	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ¬ 𝑅 ≤ 𝑊 )
5		simp12	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) )
6	4 5	jca	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( ¬ 𝑅 ≤ 𝑊 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) )
7		simp3l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → 𝑅 ∈ 𝐴 )
8		simp13	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ¬ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) )
9		ralnex	⊢ ( ∀ 𝑟 ∈ 𝐴 ¬ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ↔ ¬ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) )
10	8 9	sylibr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ∀ 𝑟 ∈ 𝐴 ¬ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) )
11		breq1	⊢ ( 𝑟 = 𝑅 → ( 𝑟 ≤ 𝑊 ↔ 𝑅 ≤ 𝑊 ) )
12	11	notbid	⊢ ( 𝑟 = 𝑅 → ( ¬ 𝑟 ≤ 𝑊 ↔ ¬ 𝑅 ≤ 𝑊 ) )
13		oveq2	⊢ ( 𝑟 = 𝑅 → ( 𝑃 ∨ 𝑟 ) = ( 𝑃 ∨ 𝑅 ) )
14		oveq2	⊢ ( 𝑟 = 𝑅 → ( 𝑄 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑅 ) )
15	13 14	eqeq12d	⊢ ( 𝑟 = 𝑅 → ( ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ↔ ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) )
16	12 15	anbi12d	⊢ ( 𝑟 = 𝑅 → ( ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ↔ ( ¬ 𝑅 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) ) )
17	16	notbid	⊢ ( 𝑟 = 𝑅 → ( ¬ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ↔ ¬ ( ¬ 𝑅 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) ) )
18	17	rspcva	⊢ ( ( 𝑅 ∈ 𝐴 ∧ ∀ 𝑟 ∈ 𝐴 ¬ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) → ¬ ( ¬ 𝑅 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) )
19	7 10 18	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ¬ ( ¬ 𝑅 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) )
20		simp11	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → 𝐾 ∈ HL )
21		hlcvl	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ CvLat )
22	20 21	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → 𝐾 ∈ CvLat )
23		simp21	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → 𝑃 ∈ 𝐴 )
24		simp22	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → 𝑄 ∈ 𝐴 )
25		simp23	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → 𝑃 ≠ 𝑄 )
26	3 1 2	cvlsupr2	⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ( ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ↔ ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
27	22 23 24 7 25 26	syl131anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ↔ ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
28	27	anbi2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( ( ¬ 𝑅 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) ↔ ( ¬ 𝑅 ≤ 𝑊 ∧ ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) )
29	19 28	mtbid	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ¬ ( ¬ 𝑅 ≤ 𝑊 ∧ ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
30		ianor	⊢ ( ¬ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ) ∧ ( ¬ 𝑅 ≤ 𝑊 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ↔ ( ¬ ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ) ∨ ¬ ( ¬ 𝑅 ≤ 𝑊 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
31		df-3an	⊢ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ↔ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) )
32	31	anbi2i	⊢ ( ( ¬ 𝑅 ≤ 𝑊 ∧ ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ↔ ( ¬ 𝑅 ≤ 𝑊 ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
33		an12	⊢ ( ( ¬ 𝑅 ≤ 𝑊 ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ↔ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ) ∧ ( ¬ 𝑅 ≤ 𝑊 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
34	32 33	bitri	⊢ ( ( ¬ 𝑅 ≤ 𝑊 ∧ ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ↔ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ) ∧ ( ¬ 𝑅 ≤ 𝑊 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
35	34	notbii	⊢ ( ¬ ( ¬ 𝑅 ≤ 𝑊 ∧ ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ↔ ¬ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ) ∧ ( ¬ 𝑅 ≤ 𝑊 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
36		pm4.62	⊢ ( ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ) → ¬ ( ¬ 𝑅 ≤ 𝑊 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ↔ ( ¬ ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ) ∨ ¬ ( ¬ 𝑅 ≤ 𝑊 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
37	30 35 36	3bitr4ri	⊢ ( ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ) → ¬ ( ¬ 𝑅 ≤ 𝑊 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ↔ ¬ ( ¬ 𝑅 ≤ 𝑊 ∧ ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
38	29 37	sylibr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ) → ¬ ( ¬ 𝑅 ≤ 𝑊 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
39	6 38	mt2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ¬ ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ) )
40		neanior	⊢ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ) ↔ ¬ ( 𝑅 = 𝑃 ∨ 𝑅 = 𝑄 ) )
41	40	con2bii	⊢ ( ( 𝑅 = 𝑃 ∨ 𝑅 = 𝑄 ) ↔ ¬ ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ) )
42	39 41	sylibr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( 𝑅 = 𝑃 ∨ 𝑅 = 𝑄 ) )