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

Metamath Proof Explorer

Theorem lvoli2

Description: The join of 4 different atoms is a lattice volume. (Contributed by NM, 8-Jul-2012)

Ref Expression
Hypotheses lvoli2.l ⊢ ≤ = ( le ‘ 𝐾 )
lvoli2.j ⊢ ∨ = ( join ‘ 𝐾 )
lvoli2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lvoli2.v ⊢ 𝑉 = ( LVols ‘ 𝐾 )
Assertion lvoli2 ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑉 )

Proof

Step Hyp Ref Expression
1 lvoli2.l ⊢ ≤ = ( le ‘ 𝐾 )
2 lvoli2.j ⊢ ∨ = ( join ‘ 𝐾 )
3 lvoli2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 lvoli2.v ⊢ 𝑉 = ( LVols ‘ 𝐾 )
5 simp12 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑃 ∈ 𝐴 )
6 simp13 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑄 ∈ 𝐴 )
7 simp3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
8 eqidd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) )
9 neeq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ≠ 𝑞 ↔ 𝑃 ≠ 𝑞 ) )
10 oveq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ∨ 𝑞 ) = ( 𝑃 ∨ 𝑞 ) )
11 10 breq2d ⊢ ( 𝑝 = 𝑃 → ( 𝑅 ≤ ( 𝑝 ∨ 𝑞 ) ↔ 𝑅 ≤ ( 𝑃 ∨ 𝑞 ) ) )
12 11 notbid ⊢ ( 𝑝 = 𝑃 → ( ¬ 𝑅 ≤ ( 𝑝 ∨ 𝑞 ) ↔ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑞 ) ) )
13 10 oveq1d ⊢ ( 𝑝 = 𝑃 → ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) = ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑅 ) )
14 13 breq2d ⊢ ( 𝑝 = 𝑃 → ( 𝑆 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ↔ 𝑆 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑅 ) ) )
15 14 notbid ⊢ ( 𝑝 = 𝑃 → ( ¬ 𝑆 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ↔ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑅 ) ) )
16 9 12 15 3anbi123d ⊢ ( 𝑝 = 𝑃 → ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑆 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ) ↔ ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑅 ) ) ) )
17 13 oveq1d ⊢ ( 𝑝 = 𝑃 → ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑆 ) )
18 17 eqeq2d ⊢ ( 𝑝 = 𝑃 → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑆 ) ↔ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑆 ) ) )
19 16 18 anbi12d ⊢ ( 𝑝 = 𝑃 → ( ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑆 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑆 ) ) ↔ ( ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑅 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑆 ) ) ) )
20 neeq2 ⊢ ( 𝑞 = 𝑄 → ( 𝑃 ≠ 𝑞 ↔ 𝑃 ≠ 𝑄 ) )
21 oveq2 ⊢ ( 𝑞 = 𝑄 → ( 𝑃 ∨ 𝑞 ) = ( 𝑃 ∨ 𝑄 ) )
22 21 breq2d ⊢ ( 𝑞 = 𝑄 → ( 𝑅 ≤ ( 𝑃 ∨ 𝑞 ) ↔ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) )
23 22 notbid ⊢ ( 𝑞 = 𝑄 → ( ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑞 ) ↔ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) )
24 21 oveq1d ⊢ ( 𝑞 = 𝑄 → ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑅 ) = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
25 24 breq2d ⊢ ( 𝑞 = 𝑄 → ( 𝑆 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑅 ) ↔ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
26 25 notbid ⊢ ( 𝑞 = 𝑄 → ( ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑅 ) ↔ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
27 20 23 26 3anbi123d ⊢ ( 𝑞 = 𝑄 → ( ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑅 ) ) ↔ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) )
28 24 oveq1d ⊢ ( 𝑞 = 𝑄 → ( ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) )
29 28 eqeq2d ⊢ ( 𝑞 = 𝑄 → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑆 ) ↔ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ) )
30 27 29 anbi12d ⊢ ( 𝑞 = 𝑄 → ( ( ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑅 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑆 ) ) ↔ ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ) ) )
31 19 30 rspc2ev ⊢ ( ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ) ) → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑆 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑆 ) ) )
32 5 6 7 8 31 syl112anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑆 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑆 ) ) )
33 32 3exp ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑆 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑆 ) ) ) ) )
34 simplrl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑆 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑆 ) ) ) → 𝑅 ∈ 𝐴 )
35 simplrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑆 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑆 ) ) ) → 𝑆 ∈ 𝐴 )
36 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑆 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑆 ) ) ) → ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑆 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑆 ) ) )
37 breq1 ⊢ ( 𝑟 = 𝑅 → ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ↔ 𝑅 ≤ ( 𝑝 ∨ 𝑞 ) ) )
38 37 notbid ⊢ ( 𝑟 = 𝑅 → ( ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ↔ ¬ 𝑅 ≤ ( 𝑝 ∨ 𝑞 ) ) )
39 oveq2 ⊢ ( 𝑟 = 𝑅 → ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) )
40 39 breq2d ⊢ ( 𝑟 = 𝑅 → ( 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ↔ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ) )
41 40 notbid ⊢ ( 𝑟 = 𝑅 → ( ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ↔ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ) )
42 38 41 3anbi23d ⊢ ( 𝑟 = 𝑅 → ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ↔ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ) ) )
43 39 oveq1d ⊢ ( 𝑟 = 𝑅 → ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑠 ) )
44 43 eqeq2d ⊢ ( 𝑟 = 𝑅 → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ↔ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑠 ) ) )
45 42 44 anbi12d ⊢ ( 𝑟 = 𝑅 → ( ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ↔ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑠 ) ) ) )
46 breq1 ⊢ ( 𝑠 = 𝑆 → ( 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ↔ 𝑆 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ) )
47 46 notbid ⊢ ( 𝑠 = 𝑆 → ( ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ↔ ¬ 𝑆 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ) )
48 47 3anbi3d ⊢ ( 𝑠 = 𝑆 → ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ) ↔ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑆 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ) ) )
49 oveq2 ⊢ ( 𝑠 = 𝑆 → ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑠 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑆 ) )
50 49 eqeq2d ⊢ ( 𝑠 = 𝑆 → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑠 ) ↔ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑆 ) ) )
51 48 50 anbi12d ⊢ ( 𝑠 = 𝑆 → ( ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑠 ) ) ↔ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑆 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑆 ) ) ) )
52 45 51 rspc2ev ⊢ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑆 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑆 ) ) ) → ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) )
53 34 35 36 52 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑆 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑆 ) ) ) → ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) )
54 53 ex ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑆 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑆 ) ) → ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
55 54 reximdv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ∃ 𝑞 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑆 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑆 ) ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
56 55 reximdv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑆 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑆 ) ) → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
57 56 ex ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑆 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑅 ) ∨ 𝑆 ) ) → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) )
58 33 57 syldd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) )
59 58 3imp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) )
60 simp11 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝐾 ∈ HL )
61 60 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝐾 ∈ Lat )
62 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
63 62 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
64 63 3ad2ant1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
65 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑅 ∈ 𝐴 )
66 62 3 atbase ⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
67 65 66 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
68 62 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
69 61 64 67 68 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
70 simp2r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑆 ∈ 𝐴 )
71 62 3 atbase ⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
72 70 71 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
73 62 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
74 61 69 72 73 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
75 62 1 2 3 4 islvol5 ⊢ ( ( 𝐾 ∈ HL ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑉 ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
76 60 74 75 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑉 ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
77 59 76 mpbird ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑉 )