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

Metamath Proof Explorer

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 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( 𝑅 = 𝑃 ∨ 𝑅 = 𝑄 ) )