Metamath Proof Explorer

Theorem 3dim2

Description: Construct 2 new layers on top of 2 given atoms. (Contributed by NM, 27-Jul-2012)

Ref Expression
Hypotheses 3dim0.j ⊒ ∨ = ( join β€˜ 𝐾 )
3dim0.l ⊒ ≀ = ( le β€˜ 𝐾 )
3dim0.a ⊒ 𝐴 = ( Atoms β€˜ 𝐾 )
Assertion 3dim2 ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) β†’ βˆƒ π‘Ÿ ∈ 𝐴 βˆƒ 𝑠 ∈ 𝐴 ( Β¬ π‘Ÿ ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ π‘Ÿ ) ) )

Proof

Step Hyp Ref Expression
1 3dim0.j ⊒ ∨ = ( join β€˜ 𝐾 )
2 3dim0.l ⊒ ≀ = ( le β€˜ 𝐾 )
3 3dim0.a ⊒ 𝐴 = ( Atoms β€˜ 𝐾 )
4 1 2 3 3dim1 ⊒ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ) β†’ βˆƒ 𝑒 ∈ 𝐴 βˆƒ 𝑣 ∈ 𝐴 βˆƒ 𝑀 ∈ 𝐴 ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) )
5 4 3adant2 ⊒ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) β†’ βˆƒ 𝑒 ∈ 𝐴 βˆƒ 𝑣 ∈ 𝐴 βˆƒ 𝑀 ∈ 𝐴 ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) )
6 simpl21 ⊒ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) β†’ 𝑒 ∈ 𝐴 )
7 simpl22 ⊒ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) β†’ 𝑣 ∈ 𝐴 )
8 simp31 ⊒ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) β†’ 𝑄 β‰  𝑒 )
9 8 necomd ⊒ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) β†’ 𝑒 β‰  𝑄 )
10 9 adantr ⊒ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) β†’ 𝑒 β‰  𝑄 )
11 oveq1 ⊒ ( 𝑃 = 𝑄 β†’ ( 𝑃 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑄 ) )
12 simp11 ⊒ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) β†’ 𝐾 ∈ HL )
13 simp13 ⊒ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) β†’ 𝑄 ∈ 𝐴 )
14 1 3 hlatjidm ⊒ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ) β†’ ( 𝑄 ∨ 𝑄 ) = 𝑄 )
15 12 13 14 syl2anc ⊒ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) β†’ ( 𝑄 ∨ 𝑄 ) = 𝑄 )
16 11 15 sylan9eqr ⊒ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) β†’ ( 𝑃 ∨ 𝑄 ) = 𝑄 )
17 16 breq2d ⊒ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) β†’ ( 𝑒 ≀ ( 𝑃 ∨ 𝑄 ) ↔ 𝑒 ≀ 𝑄 ) )
18 17 notbid ⊒ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) β†’ ( Β¬ 𝑒 ≀ ( 𝑃 ∨ 𝑄 ) ↔ Β¬ 𝑒 ≀ 𝑄 ) )
19 hlatl ⊒ ( 𝐾 ∈ HL β†’ 𝐾 ∈ AtLat )
20 12 19 syl ⊒ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) β†’ 𝐾 ∈ AtLat )
21 simp21 ⊒ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) β†’ 𝑒 ∈ 𝐴 )
22 2 3 atncmp ⊒ ( ( 𝐾 ∈ AtLat ∧ 𝑒 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) β†’ ( Β¬ 𝑒 ≀ 𝑄 ↔ 𝑒 β‰  𝑄 ) )
23 20 21 13 22 syl3anc ⊒ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) β†’ ( Β¬ 𝑒 ≀ 𝑄 ↔ 𝑒 β‰  𝑄 ) )
24 23 adantr ⊒ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) β†’ ( Β¬ 𝑒 ≀ 𝑄 ↔ 𝑒 β‰  𝑄 ) )
25 18 24 bitrd ⊒ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) β†’ ( Β¬ 𝑒 ≀ ( 𝑃 ∨ 𝑄 ) ↔ 𝑒 β‰  𝑄 ) )
26 10 25 mpbird ⊒ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) β†’ Β¬ 𝑒 ≀ ( 𝑃 ∨ 𝑄 ) )
27 simpl32 ⊒ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) β†’ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) )
28 16 oveq1d ⊒ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) β†’ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) = ( 𝑄 ∨ 𝑒 ) )
29 28 breq2d ⊒ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) β†’ ( 𝑣 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) ↔ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ) )
30 27 29 mtbird ⊒ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) β†’ Β¬ 𝑣 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) )
31 breq1 ⊒ ( π‘Ÿ = 𝑒 β†’ ( π‘Ÿ ≀ ( 𝑃 ∨ 𝑄 ) ↔ 𝑒 ≀ ( 𝑃 ∨ 𝑄 ) ) )
32 31 notbid ⊒ ( π‘Ÿ = 𝑒 β†’ ( Β¬ π‘Ÿ ≀ ( 𝑃 ∨ 𝑄 ) ↔ Β¬ 𝑒 ≀ ( 𝑃 ∨ 𝑄 ) ) )
33 oveq2 ⊒ ( π‘Ÿ = 𝑒 β†’ ( ( 𝑃 ∨ 𝑄 ) ∨ π‘Ÿ ) = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) )
34 33 breq2d ⊒ ( π‘Ÿ = 𝑒 β†’ ( 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ π‘Ÿ ) ↔ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) ) )
35 34 notbid ⊒ ( π‘Ÿ = 𝑒 β†’ ( Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ π‘Ÿ ) ↔ Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) ) )
36 32 35 anbi12d ⊒ ( π‘Ÿ = 𝑒 β†’ ( ( Β¬ π‘Ÿ ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ π‘Ÿ ) ) ↔ ( Β¬ 𝑒 ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) ) ) )
37 breq1 ⊒ ( 𝑠 = 𝑣 β†’ ( 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) ↔ 𝑣 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) ) )
38 37 notbid ⊒ ( 𝑠 = 𝑣 β†’ ( Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) ↔ Β¬ 𝑣 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) ) )
39 38 anbi2d ⊒ ( 𝑠 = 𝑣 β†’ ( ( Β¬ 𝑒 ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) ) ↔ ( Β¬ 𝑒 ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑣 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) ) ) )
40 36 39 rspc2ev ⊒ ( ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ ( Β¬ 𝑒 ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑣 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) ) ) β†’ βˆƒ π‘Ÿ ∈ 𝐴 βˆƒ 𝑠 ∈ 𝐴 ( Β¬ π‘Ÿ ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ π‘Ÿ ) ) )
41 6 7 26 30 40 syl112anc ⊒ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) β†’ βˆƒ π‘Ÿ ∈ 𝐴 βˆƒ 𝑠 ∈ 𝐴 ( Β¬ π‘Ÿ ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ π‘Ÿ ) ) )
42 simp22 ⊒ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) β†’ 𝑣 ∈ 𝐴 )
43 simp23 ⊒ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) β†’ 𝑀 ∈ 𝐴 )
44 42 43 jca ⊒ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) β†’ ( 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) )
45 44 ad2antrr ⊒ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 β‰  𝑄 ) ∧ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) ) β†’ ( 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) )
46 simpll1 ⊒ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 β‰  𝑄 ) ∧ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) ) β†’ ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) )
47 simp32 ⊒ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) β†’ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) )
48 simp33 ⊒ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) β†’ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) )
49 21 47 48 3jca ⊒ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) β†’ ( 𝑒 ∈ 𝐴 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) )
50 49 ad2antrr ⊒ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 β‰  𝑄 ) ∧ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) ) β†’ ( 𝑒 ∈ 𝐴 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) )
51 simplr ⊒ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 β‰  𝑄 ) ∧ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) ) β†’ 𝑃 β‰  𝑄 )
52 simpr ⊒ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 β‰  𝑄 ) ∧ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) ) β†’ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) )
53 1 2 3 3dimlem2 ⊒ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ∧ ( 𝑃 β‰  𝑄 ∧ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) ) ) β†’ ( 𝑃 β‰  𝑄 ∧ Β¬ 𝑣 ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ) )
54 46 50 51 52 53 syl112anc ⊒ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 β‰  𝑄 ) ∧ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) ) β†’ ( 𝑃 β‰  𝑄 ∧ Β¬ 𝑣 ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ) )
55 3simpc ⊒ ( ( 𝑃 β‰  𝑄 ∧ Β¬ 𝑣 ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ) β†’ ( Β¬ 𝑣 ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ) )
56 54 55 syl ⊒ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 β‰  𝑄 ) ∧ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) ) β†’ ( Β¬ 𝑣 ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ) )
57 breq1 ⊒ ( π‘Ÿ = 𝑣 β†’ ( π‘Ÿ ≀ ( 𝑃 ∨ 𝑄 ) ↔ 𝑣 ≀ ( 𝑃 ∨ 𝑄 ) ) )
58 57 notbid ⊒ ( π‘Ÿ = 𝑣 β†’ ( Β¬ π‘Ÿ ≀ ( 𝑃 ∨ 𝑄 ) ↔ Β¬ 𝑣 ≀ ( 𝑃 ∨ 𝑄 ) ) )
59 oveq2 ⊒ ( π‘Ÿ = 𝑣 β†’ ( ( 𝑃 ∨ 𝑄 ) ∨ π‘Ÿ ) = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) )
60 59 breq2d ⊒ ( π‘Ÿ = 𝑣 β†’ ( 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ π‘Ÿ ) ↔ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ) )
61 60 notbid ⊒ ( π‘Ÿ = 𝑣 β†’ ( Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ π‘Ÿ ) ↔ Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ) )
62 58 61 anbi12d ⊒ ( π‘Ÿ = 𝑣 β†’ ( ( Β¬ π‘Ÿ ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ π‘Ÿ ) ) ↔ ( Β¬ 𝑣 ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ) ) )
63 breq1 ⊒ ( 𝑠 = 𝑀 β†’ ( 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ↔ 𝑀 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ) )
64 63 notbid ⊒ ( 𝑠 = 𝑀 β†’ ( Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ↔ Β¬ 𝑀 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ) )
65 64 anbi2d ⊒ ( 𝑠 = 𝑀 β†’ ( ( Β¬ 𝑣 ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ) ↔ ( Β¬ 𝑣 ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ) ) )
66 62 65 rspc2ev ⊒ ( ( 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ∧ ( Β¬ 𝑣 ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ) ) β†’ βˆƒ π‘Ÿ ∈ 𝐴 βˆƒ 𝑠 ∈ 𝐴 ( Β¬ π‘Ÿ ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ π‘Ÿ ) ) )
67 66 3expa ⊒ ( ( ( 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( Β¬ 𝑣 ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ) ) β†’ βˆƒ π‘Ÿ ∈ 𝐴 βˆƒ 𝑠 ∈ 𝐴 ( Β¬ π‘Ÿ ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ π‘Ÿ ) ) )
68 45 56 67 syl2anc ⊒ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 β‰  𝑄 ) ∧ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) ) β†’ βˆƒ π‘Ÿ ∈ 𝐴 βˆƒ 𝑠 ∈ 𝐴 ( Β¬ π‘Ÿ ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ π‘Ÿ ) ) )
69 21 43 jca ⊒ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) β†’ ( 𝑒 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) )
70 69 ad3antrrr ⊒ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 β‰  𝑄 ) ∧ Β¬ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) ) ∧ 𝑃 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) β†’ ( 𝑒 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) )
71 simp1 ⊒ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) β†’ ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) )
72 21 42 jca ⊒ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) β†’ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) )
73 8 48 jca ⊒ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) β†’ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) )
74 71 72 73 3jca ⊒ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) β†’ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) )
75 74 ad3antrrr ⊒ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 β‰  𝑄 ) ∧ Β¬ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) ) ∧ 𝑃 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) β†’ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) )
76 simpllr ⊒ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 β‰  𝑄 ) ∧ Β¬ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) ) ∧ 𝑃 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) β†’ 𝑃 β‰  𝑄 )
77 simplr ⊒ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 β‰  𝑄 ) ∧ Β¬ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) ) ∧ 𝑃 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) β†’ Β¬ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) )
78 simpr ⊒ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 β‰  𝑄 ) ∧ Β¬ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) ) ∧ 𝑃 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) β†’ 𝑃 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) )
79 1 2 3 3dimlem3 ⊒ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ ( 𝑃 β‰  𝑄 ∧ Β¬ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) ∧ 𝑃 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) β†’ ( 𝑃 β‰  𝑄 ∧ Β¬ 𝑒 ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) ) )
80 75 76 77 78 79 syl13anc ⊒ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 β‰  𝑄 ) ∧ Β¬ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) ) ∧ 𝑃 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) β†’ ( 𝑃 β‰  𝑄 ∧ Β¬ 𝑒 ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) ) )
81 3simpc ⊒ ( ( 𝑃 β‰  𝑄 ∧ Β¬ 𝑒 ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) ) β†’ ( Β¬ 𝑒 ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) ) )
82 80 81 syl ⊒ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 β‰  𝑄 ) ∧ Β¬ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) ) ∧ 𝑃 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) β†’ ( Β¬ 𝑒 ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) ) )
83 breq1 ⊒ ( 𝑠 = 𝑀 β†’ ( 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) ↔ 𝑀 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) ) )
84 83 notbid ⊒ ( 𝑠 = 𝑀 β†’ ( Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) ↔ Β¬ 𝑀 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) ) )
85 84 anbi2d ⊒ ( 𝑠 = 𝑀 β†’ ( ( Β¬ 𝑒 ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) ) ↔ ( Β¬ 𝑒 ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) ) ) )
86 36 85 rspc2ev ⊒ ( ( 𝑒 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ∧ ( Β¬ 𝑒 ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) ) ) β†’ βˆƒ π‘Ÿ ∈ 𝐴 βˆƒ 𝑠 ∈ 𝐴 ( Β¬ π‘Ÿ ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ π‘Ÿ ) ) )
87 86 3expa ⊒ ( ( ( 𝑒 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( Β¬ 𝑒 ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) ) ) β†’ βˆƒ π‘Ÿ ∈ 𝐴 βˆƒ 𝑠 ∈ 𝐴 ( Β¬ π‘Ÿ ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ π‘Ÿ ) ) )
88 70 82 87 syl2anc ⊒ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 β‰  𝑄 ) ∧ Β¬ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) ) ∧ 𝑃 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) β†’ βˆƒ π‘Ÿ ∈ 𝐴 βˆƒ 𝑠 ∈ 𝐴 ( Β¬ π‘Ÿ ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ π‘Ÿ ) ) )
89 72 ad3antrrr ⊒ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 β‰  𝑄 ) ∧ Β¬ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) ) ∧ Β¬ 𝑃 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) β†’ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) )
90 8 47 jca ⊒ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) β†’ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ) )
91 71 72 90 3jca ⊒ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) β†’ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ) ) )
92 91 ad3antrrr ⊒ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 β‰  𝑄 ) ∧ Β¬ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) ) ∧ Β¬ 𝑃 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) β†’ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ) ) )
93 simpllr ⊒ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 β‰  𝑄 ) ∧ Β¬ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) ) ∧ Β¬ 𝑃 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) β†’ 𝑃 β‰  𝑄 )
94 simplr ⊒ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 β‰  𝑄 ) ∧ Β¬ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) ) ∧ Β¬ 𝑃 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) β†’ Β¬ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) )
95 simpr ⊒ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 β‰  𝑄 ) ∧ Β¬ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) ) ∧ Β¬ 𝑃 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) β†’ Β¬ 𝑃 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) )
96 1 2 3 3dimlem4 ⊒ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ) ) ∧ ( 𝑃 β‰  𝑄 ∧ Β¬ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) ) ∧ Β¬ 𝑃 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) β†’ ( 𝑃 β‰  𝑄 ∧ Β¬ 𝑒 ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑣 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) ) )
97 92 93 94 95 96 syl121anc ⊒ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 β‰  𝑄 ) ∧ Β¬ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) ) ∧ Β¬ 𝑃 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) β†’ ( 𝑃 β‰  𝑄 ∧ Β¬ 𝑒 ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑣 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) ) )
98 3simpc ⊒ ( ( 𝑃 β‰  𝑄 ∧ Β¬ 𝑒 ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑣 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) ) β†’ ( Β¬ 𝑒 ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑣 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) ) )
99 97 98 syl ⊒ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 β‰  𝑄 ) ∧ Β¬ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) ) ∧ Β¬ 𝑃 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) β†’ ( Β¬ 𝑒 ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑣 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) ) )
100 40 3expa ⊒ ( ( ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( Β¬ 𝑒 ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑣 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑒 ) ) ) β†’ βˆƒ π‘Ÿ ∈ 𝐴 βˆƒ 𝑠 ∈ 𝐴 ( Β¬ π‘Ÿ ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ π‘Ÿ ) ) )
101 89 99 100 syl2anc ⊒ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 β‰  𝑄 ) ∧ Β¬ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) ) ∧ Β¬ 𝑃 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) β†’ βˆƒ π‘Ÿ ∈ 𝐴 βˆƒ 𝑠 ∈ 𝐴 ( Β¬ π‘Ÿ ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ π‘Ÿ ) ) )
102 88 101 pm2.61dan ⊒ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 β‰  𝑄 ) ∧ Β¬ 𝑃 ≀ ( 𝑄 ∨ 𝑒 ) ) β†’ βˆƒ π‘Ÿ ∈ 𝐴 βˆƒ 𝑠 ∈ 𝐴 ( Β¬ π‘Ÿ ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ π‘Ÿ ) ) )
103 68 102 pm2.61dan ⊒ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) ∧ 𝑃 β‰  𝑄 ) β†’ βˆƒ π‘Ÿ ∈ 𝐴 βˆƒ 𝑠 ∈ 𝐴 ( Β¬ π‘Ÿ ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ π‘Ÿ ) ) )
104 41 103 pm2.61dane ⊒ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ∧ ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) ) β†’ βˆƒ π‘Ÿ ∈ 𝐴 βˆƒ 𝑠 ∈ 𝐴 ( Β¬ π‘Ÿ ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ π‘Ÿ ) ) )
105 104 3exp ⊒ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) β†’ ( ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) β†’ ( ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) β†’ βˆƒ π‘Ÿ ∈ 𝐴 βˆƒ 𝑠 ∈ 𝐴 ( Β¬ π‘Ÿ ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ π‘Ÿ ) ) ) ) )
106 105 3expd ⊒ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) β†’ ( 𝑒 ∈ 𝐴 β†’ ( 𝑣 ∈ 𝐴 β†’ ( 𝑀 ∈ 𝐴 β†’ ( ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) β†’ βˆƒ π‘Ÿ ∈ 𝐴 βˆƒ 𝑠 ∈ 𝐴 ( Β¬ π‘Ÿ ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ π‘Ÿ ) ) ) ) ) ) )
107 106 imp32 ⊒ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) β†’ ( 𝑀 ∈ 𝐴 β†’ ( ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) β†’ βˆƒ π‘Ÿ ∈ 𝐴 βˆƒ 𝑠 ∈ 𝐴 ( Β¬ π‘Ÿ ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ π‘Ÿ ) ) ) ) )
108 107 rexlimdv ⊒ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) β†’ ( βˆƒ 𝑀 ∈ 𝐴 ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) β†’ βˆƒ π‘Ÿ ∈ 𝐴 βˆƒ 𝑠 ∈ 𝐴 ( Β¬ π‘Ÿ ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ π‘Ÿ ) ) ) )
109 108 rexlimdvva ⊒ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) β†’ ( βˆƒ 𝑒 ∈ 𝐴 βˆƒ 𝑣 ∈ 𝐴 βˆƒ 𝑀 ∈ 𝐴 ( 𝑄 β‰  𝑒 ∧ Β¬ 𝑣 ≀ ( 𝑄 ∨ 𝑒 ) ∧ Β¬ 𝑀 ≀ ( ( 𝑄 ∨ 𝑒 ) ∨ 𝑣 ) ) β†’ βˆƒ π‘Ÿ ∈ 𝐴 βˆƒ 𝑠 ∈ 𝐴 ( Β¬ π‘Ÿ ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ π‘Ÿ ) ) ) )
110 5 109 mpd ⊒ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) β†’ βˆƒ π‘Ÿ ∈ 𝐴 βˆƒ 𝑠 ∈ 𝐴 ( Β¬ π‘Ÿ ≀ ( 𝑃 ∨ 𝑄 ) ∧ Β¬ 𝑠 ≀ ( ( 𝑃 ∨ 𝑄 ) ∨ π‘Ÿ ) ) )