Metamath Proof Explorer


Theorem cdleme20g

Description: Part of proof of Lemma E in Crawley p. 113, last paragraph on p. 114, antepenultimate line. D , F , Y , G represent s_2, f(s), t_2, f(t). (Contributed by NM, 18-Nov-2012)

Ref Expression
Hypotheses cdleme19.l ⊢ ≤ = ( le ā€˜ š¾ )
cdleme19.j ⊢ ∨ = ( join ā€˜ š¾ )
cdleme19.m ⊢ ∧ = ( meet ā€˜ š¾ )
cdleme19.a ⊢ š“ = ( Atoms ā€˜ š¾ )
cdleme19.h ⊢ š» = ( LHyp ā€˜ š¾ )
cdleme19.u ⊢ š‘ˆ = ( ( š‘ƒ ∨ š‘„ ) ∧ š‘Š )
cdleme19.f ⊢ š¹ = ( ( š‘† ∨ š‘ˆ ) ∧ ( š‘„ ∨ ( ( š‘ƒ ∨ š‘† ) ∧ š‘Š ) ) )
cdleme19.g ⊢ šŗ = ( ( š‘‡ ∨ š‘ˆ ) ∧ ( š‘„ ∨ ( ( š‘ƒ ∨ š‘‡ ) ∧ š‘Š ) ) )
cdleme19.d ⊢ š· = ( ( š‘… ∨ š‘† ) ∧ š‘Š )
cdleme19.y ⊢ š‘Œ = ( ( š‘… ∨ š‘‡ ) ∧ š‘Š )
cdleme20.v ⊢ š‘‰ = ( ( š‘† ∨ š‘‡ ) ∧ š‘Š )
Assertion cdleme20g ( ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘ƒ ∈ š“ ∧ ¬ š‘ƒ ≤ š‘Š ) ∧ ( š‘„ ∈ š“ ∧ ¬ š‘„ ≤ š‘Š ) ) ∧ ( ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ∧ ( š‘… ∈ š“ ∧ ¬ š‘… ≤ š‘Š ) ) ∧ ( ( š‘ƒ ≠ š‘„ ∧ š‘† ≠ š‘‡ ) ∧ ( ¬ š‘† ≤ ( š‘ƒ ∨ š‘„ ) ∧ ¬ š‘‡ ≤ ( š‘ƒ ∨ š‘„ ) ) ∧ š‘… ≤ ( š‘ƒ ∨ š‘„ ) ) ) → ( ( ( š· ∨ š‘† ) ∧ ( š‘Œ ∨ š‘‡ ) ) ∨ ( ( š‘† ∨ š¹ ) ∧ ( š‘‡ ∨ šŗ ) ) ) = ( ( ( š‘† ∨ š‘… ) ∧ ( š‘‡ ∨ š‘… ) ) ∨ ( ( š‘† ∨ š‘ˆ ) ∧ ( š‘‡ ∨ š‘ˆ ) ) ) )

Proof

Step Hyp Ref Expression
1 cdleme19.l ⊢ ≤ = ( le ā€˜ š¾ )
2 cdleme19.j ⊢ ∨ = ( join ā€˜ š¾ )
3 cdleme19.m ⊢ ∧ = ( meet ā€˜ š¾ )
4 cdleme19.a ⊢ š“ = ( Atoms ā€˜ š¾ )
5 cdleme19.h ⊢ š» = ( LHyp ā€˜ š¾ )
6 cdleme19.u ⊢ š‘ˆ = ( ( š‘ƒ ∨ š‘„ ) ∧ š‘Š )
7 cdleme19.f ⊢ š¹ = ( ( š‘† ∨ š‘ˆ ) ∧ ( š‘„ ∨ ( ( š‘ƒ ∨ š‘† ) ∧ š‘Š ) ) )
8 cdleme19.g ⊢ šŗ = ( ( š‘‡ ∨ š‘ˆ ) ∧ ( š‘„ ∨ ( ( š‘ƒ ∨ š‘‡ ) ∧ š‘Š ) ) )
9 cdleme19.d ⊢ š· = ( ( š‘… ∨ š‘† ) ∧ š‘Š )
10 cdleme19.y ⊢ š‘Œ = ( ( š‘… ∨ š‘‡ ) ∧ š‘Š )
11 cdleme20.v ⊢ š‘‰ = ( ( š‘† ∨ š‘‡ ) ∧ š‘Š )
12 simp11l ⊢ ( ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘ƒ ∈ š“ ∧ ¬ š‘ƒ ≤ š‘Š ) ∧ ( š‘„ ∈ š“ ∧ ¬ š‘„ ≤ š‘Š ) ) ∧ ( ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ∧ ( š‘… ∈ š“ ∧ ¬ š‘… ≤ š‘Š ) ) ∧ ( ( š‘ƒ ≠ š‘„ ∧ š‘† ≠ š‘‡ ) ∧ ( ¬ š‘† ≤ ( š‘ƒ ∨ š‘„ ) ∧ ¬ š‘‡ ≤ ( š‘ƒ ∨ š‘„ ) ) ∧ š‘… ≤ ( š‘ƒ ∨ š‘„ ) ) ) → š¾ ∈ HL )
13 simp11r ⊢ ( ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘ƒ ∈ š“ ∧ ¬ š‘ƒ ≤ š‘Š ) ∧ ( š‘„ ∈ š“ ∧ ¬ š‘„ ≤ š‘Š ) ) ∧ ( ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ∧ ( š‘… ∈ š“ ∧ ¬ š‘… ≤ š‘Š ) ) ∧ ( ( š‘ƒ ≠ š‘„ ∧ š‘† ≠ š‘‡ ) ∧ ( ¬ š‘† ≤ ( š‘ƒ ∨ š‘„ ) ∧ ¬ š‘‡ ≤ ( š‘ƒ ∨ š‘„ ) ) ∧ š‘… ≤ ( š‘ƒ ∨ š‘„ ) ) ) → š‘Š ∈ š» )
14 simp21l ⊢ ( ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘ƒ ∈ š“ ∧ ¬ š‘ƒ ≤ š‘Š ) ∧ ( š‘„ ∈ š“ ∧ ¬ š‘„ ≤ š‘Š ) ) ∧ ( ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ∧ ( š‘… ∈ š“ ∧ ¬ š‘… ≤ š‘Š ) ) ∧ ( ( š‘ƒ ≠ š‘„ ∧ š‘† ≠ š‘‡ ) ∧ ( ¬ š‘† ≤ ( š‘ƒ ∨ š‘„ ) ∧ ¬ š‘‡ ≤ ( š‘ƒ ∨ š‘„ ) ) ∧ š‘… ≤ ( š‘ƒ ∨ š‘„ ) ) ) → š‘† ∈ š“ )
15 simp21r ⊢ ( ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘ƒ ∈ š“ ∧ ¬ š‘ƒ ≤ š‘Š ) ∧ ( š‘„ ∈ š“ ∧ ¬ š‘„ ≤ š‘Š ) ) ∧ ( ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ∧ ( š‘… ∈ š“ ∧ ¬ š‘… ≤ š‘Š ) ) ∧ ( ( š‘ƒ ≠ š‘„ ∧ š‘† ≠ š‘‡ ) ∧ ( ¬ š‘† ≤ ( š‘ƒ ∨ š‘„ ) ∧ ¬ š‘‡ ≤ ( š‘ƒ ∨ š‘„ ) ) ∧ š‘… ≤ ( š‘ƒ ∨ š‘„ ) ) ) → ¬ š‘† ≤ š‘Š )
16 simp23l ⊢ ( ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘ƒ ∈ š“ ∧ ¬ š‘ƒ ≤ š‘Š ) ∧ ( š‘„ ∈ š“ ∧ ¬ š‘„ ≤ š‘Š ) ) ∧ ( ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ∧ ( š‘… ∈ š“ ∧ ¬ š‘… ≤ š‘Š ) ) ∧ ( ( š‘ƒ ≠ š‘„ ∧ š‘† ≠ š‘‡ ) ∧ ( ¬ š‘† ≤ ( š‘ƒ ∨ š‘„ ) ∧ ¬ š‘‡ ≤ ( š‘ƒ ∨ š‘„ ) ) ∧ š‘… ≤ ( š‘ƒ ∨ š‘„ ) ) ) → š‘… ∈ š“ )
17 simp33 ⊢ ( ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘ƒ ∈ š“ ∧ ¬ š‘ƒ ≤ š‘Š ) ∧ ( š‘„ ∈ š“ ∧ ¬ š‘„ ≤ š‘Š ) ) ∧ ( ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ∧ ( š‘… ∈ š“ ∧ ¬ š‘… ≤ š‘Š ) ) ∧ ( ( š‘ƒ ≠ š‘„ ∧ š‘† ≠ š‘‡ ) ∧ ( ¬ š‘† ≤ ( š‘ƒ ∨ š‘„ ) ∧ ¬ š‘‡ ≤ ( š‘ƒ ∨ š‘„ ) ) ∧ š‘… ≤ ( š‘ƒ ∨ š‘„ ) ) ) → š‘… ≤ ( š‘ƒ ∨ š‘„ ) )
18 simp32l ⊢ ( ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘ƒ ∈ š“ ∧ ¬ š‘ƒ ≤ š‘Š ) ∧ ( š‘„ ∈ š“ ∧ ¬ š‘„ ≤ š‘Š ) ) ∧ ( ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ∧ ( š‘… ∈ š“ ∧ ¬ š‘… ≤ š‘Š ) ) ∧ ( ( š‘ƒ ≠ š‘„ ∧ š‘† ≠ š‘‡ ) ∧ ( ¬ š‘† ≤ ( š‘ƒ ∨ š‘„ ) ∧ ¬ š‘‡ ≤ ( š‘ƒ ∨ š‘„ ) ) ∧ š‘… ≤ ( š‘ƒ ∨ š‘„ ) ) ) → ¬ š‘† ≤ ( š‘ƒ ∨ š‘„ ) )
19 1 2 3 4 5 9 cdlemeda ⊢ ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ∧ ( š‘… ∈ š“ ∧ š‘… ≤ ( š‘ƒ ∨ š‘„ ) ∧ ¬ š‘† ≤ ( š‘ƒ ∨ š‘„ ) ) ) → š· ∈ š“ )
20 12 13 14 15 16 17 18 19 syl223anc ⊢ ( ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘ƒ ∈ š“ ∧ ¬ š‘ƒ ≤ š‘Š ) ∧ ( š‘„ ∈ š“ ∧ ¬ š‘„ ≤ š‘Š ) ) ∧ ( ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ∧ ( š‘… ∈ š“ ∧ ¬ š‘… ≤ š‘Š ) ) ∧ ( ( š‘ƒ ≠ š‘„ ∧ š‘† ≠ š‘‡ ) ∧ ( ¬ š‘† ≤ ( š‘ƒ ∨ š‘„ ) ∧ ¬ š‘‡ ≤ ( š‘ƒ ∨ š‘„ ) ) ∧ š‘… ≤ ( š‘ƒ ∨ š‘„ ) ) ) → š· ∈ š“ )
21 2 4 hlatjcom ⊢ ( ( š¾ ∈ HL ∧ š· ∈ š“ ∧ š‘† ∈ š“ ) → ( š· ∨ š‘† ) = ( š‘† ∨ š· ) )
22 12 20 14 21 syl3anc ⊢ ( ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘ƒ ∈ š“ ∧ ¬ š‘ƒ ≤ š‘Š ) ∧ ( š‘„ ∈ š“ ∧ ¬ š‘„ ≤ š‘Š ) ) ∧ ( ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ∧ ( š‘… ∈ š“ ∧ ¬ š‘… ≤ š‘Š ) ) ∧ ( ( š‘ƒ ≠ š‘„ ∧ š‘† ≠ š‘‡ ) ∧ ( ¬ š‘† ≤ ( š‘ƒ ∨ š‘„ ) ∧ ¬ š‘‡ ≤ ( š‘ƒ ∨ š‘„ ) ) ∧ š‘… ≤ ( š‘ƒ ∨ š‘„ ) ) ) → ( š· ∨ š‘† ) = ( š‘† ∨ š· ) )
23 1 2 3 4 5 9 cdleme10 ⊢ ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ š‘… ∈ š“ ∧ ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ) → ( š‘† ∨ š· ) = ( š‘† ∨ š‘… ) )
24 12 13 16 14 15 23 syl212anc ⊢ ( ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘ƒ ∈ š“ ∧ ¬ š‘ƒ ≤ š‘Š ) ∧ ( š‘„ ∈ š“ ∧ ¬ š‘„ ≤ š‘Š ) ) ∧ ( ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ∧ ( š‘… ∈ š“ ∧ ¬ š‘… ≤ š‘Š ) ) ∧ ( ( š‘ƒ ≠ š‘„ ∧ š‘† ≠ š‘‡ ) ∧ ( ¬ š‘† ≤ ( š‘ƒ ∨ š‘„ ) ∧ ¬ š‘‡ ≤ ( š‘ƒ ∨ š‘„ ) ) ∧ š‘… ≤ ( š‘ƒ ∨ š‘„ ) ) ) → ( š‘† ∨ š· ) = ( š‘† ∨ š‘… ) )
25 22 24 eqtrd ⊢ ( ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘ƒ ∈ š“ ∧ ¬ š‘ƒ ≤ š‘Š ) ∧ ( š‘„ ∈ š“ ∧ ¬ š‘„ ≤ š‘Š ) ) ∧ ( ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ∧ ( š‘… ∈ š“ ∧ ¬ š‘… ≤ š‘Š ) ) ∧ ( ( š‘ƒ ≠ š‘„ ∧ š‘† ≠ š‘‡ ) ∧ ( ¬ š‘† ≤ ( š‘ƒ ∨ š‘„ ) ∧ ¬ š‘‡ ≤ ( š‘ƒ ∨ š‘„ ) ) ∧ š‘… ≤ ( š‘ƒ ∨ š‘„ ) ) ) → ( š· ∨ š‘† ) = ( š‘† ∨ š‘… ) )
26 simp22l ⊢ ( ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘ƒ ∈ š“ ∧ ¬ š‘ƒ ≤ š‘Š ) ∧ ( š‘„ ∈ š“ ∧ ¬ š‘„ ≤ š‘Š ) ) ∧ ( ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ∧ ( š‘… ∈ š“ ∧ ¬ š‘… ≤ š‘Š ) ) ∧ ( ( š‘ƒ ≠ š‘„ ∧ š‘† ≠ š‘‡ ) ∧ ( ¬ š‘† ≤ ( š‘ƒ ∨ š‘„ ) ∧ ¬ š‘‡ ≤ ( š‘ƒ ∨ š‘„ ) ) ∧ š‘… ≤ ( š‘ƒ ∨ š‘„ ) ) ) → š‘‡ ∈ š“ )
27 simp22r ⊢ ( ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘ƒ ∈ š“ ∧ ¬ š‘ƒ ≤ š‘Š ) ∧ ( š‘„ ∈ š“ ∧ ¬ š‘„ ≤ š‘Š ) ) ∧ ( ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ∧ ( š‘… ∈ š“ ∧ ¬ š‘… ≤ š‘Š ) ) ∧ ( ( š‘ƒ ≠ š‘„ ∧ š‘† ≠ š‘‡ ) ∧ ( ¬ š‘† ≤ ( š‘ƒ ∨ š‘„ ) ∧ ¬ š‘‡ ≤ ( š‘ƒ ∨ š‘„ ) ) ∧ š‘… ≤ ( š‘ƒ ∨ š‘„ ) ) ) → ¬ š‘‡ ≤ š‘Š )
28 simp32r ⊢ ( ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘ƒ ∈ š“ ∧ ¬ š‘ƒ ≤ š‘Š ) ∧ ( š‘„ ∈ š“ ∧ ¬ š‘„ ≤ š‘Š ) ) ∧ ( ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ∧ ( š‘… ∈ š“ ∧ ¬ š‘… ≤ š‘Š ) ) ∧ ( ( š‘ƒ ≠ š‘„ ∧ š‘† ≠ š‘‡ ) ∧ ( ¬ š‘† ≤ ( š‘ƒ ∨ š‘„ ) ∧ ¬ š‘‡ ≤ ( š‘ƒ ∨ š‘„ ) ) ∧ š‘… ≤ ( š‘ƒ ∨ š‘„ ) ) ) → ¬ š‘‡ ≤ ( š‘ƒ ∨ š‘„ ) )
29 1 2 3 4 5 10 cdlemeda ⊢ ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ∧ ( š‘… ∈ š“ ∧ š‘… ≤ ( š‘ƒ ∨ š‘„ ) ∧ ¬ š‘‡ ≤ ( š‘ƒ ∨ š‘„ ) ) ) → š‘Œ ∈ š“ )
30 12 13 26 27 16 17 28 29 syl223anc ⊢ ( ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘ƒ ∈ š“ ∧ ¬ š‘ƒ ≤ š‘Š ) ∧ ( š‘„ ∈ š“ ∧ ¬ š‘„ ≤ š‘Š ) ) ∧ ( ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ∧ ( š‘… ∈ š“ ∧ ¬ š‘… ≤ š‘Š ) ) ∧ ( ( š‘ƒ ≠ š‘„ ∧ š‘† ≠ š‘‡ ) ∧ ( ¬ š‘† ≤ ( š‘ƒ ∨ š‘„ ) ∧ ¬ š‘‡ ≤ ( š‘ƒ ∨ š‘„ ) ) ∧ š‘… ≤ ( š‘ƒ ∨ š‘„ ) ) ) → š‘Œ ∈ š“ )
31 2 4 hlatjcom ⊢ ( ( š¾ ∈ HL ∧ š‘Œ ∈ š“ ∧ š‘‡ ∈ š“ ) → ( š‘Œ ∨ š‘‡ ) = ( š‘‡ ∨ š‘Œ ) )
32 12 30 26 31 syl3anc ⊢ ( ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘ƒ ∈ š“ ∧ ¬ š‘ƒ ≤ š‘Š ) ∧ ( š‘„ ∈ š“ ∧ ¬ š‘„ ≤ š‘Š ) ) ∧ ( ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ∧ ( š‘… ∈ š“ ∧ ¬ š‘… ≤ š‘Š ) ) ∧ ( ( š‘ƒ ≠ š‘„ ∧ š‘† ≠ š‘‡ ) ∧ ( ¬ š‘† ≤ ( š‘ƒ ∨ š‘„ ) ∧ ¬ š‘‡ ≤ ( š‘ƒ ∨ š‘„ ) ) ∧ š‘… ≤ ( š‘ƒ ∨ š‘„ ) ) ) → ( š‘Œ ∨ š‘‡ ) = ( š‘‡ ∨ š‘Œ ) )
33 1 2 3 4 5 10 cdleme10 ⊢ ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ š‘… ∈ š“ ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ) → ( š‘‡ ∨ š‘Œ ) = ( š‘‡ ∨ š‘… ) )
34 12 13 16 26 27 33 syl212anc ⊢ ( ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘ƒ ∈ š“ ∧ ¬ š‘ƒ ≤ š‘Š ) ∧ ( š‘„ ∈ š“ ∧ ¬ š‘„ ≤ š‘Š ) ) ∧ ( ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ∧ ( š‘… ∈ š“ ∧ ¬ š‘… ≤ š‘Š ) ) ∧ ( ( š‘ƒ ≠ š‘„ ∧ š‘† ≠ š‘‡ ) ∧ ( ¬ š‘† ≤ ( š‘ƒ ∨ š‘„ ) ∧ ¬ š‘‡ ≤ ( š‘ƒ ∨ š‘„ ) ) ∧ š‘… ≤ ( š‘ƒ ∨ š‘„ ) ) ) → ( š‘‡ ∨ š‘Œ ) = ( š‘‡ ∨ š‘… ) )
35 32 34 eqtrd ⊢ ( ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘ƒ ∈ š“ ∧ ¬ š‘ƒ ≤ š‘Š ) ∧ ( š‘„ ∈ š“ ∧ ¬ š‘„ ≤ š‘Š ) ) ∧ ( ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ∧ ( š‘… ∈ š“ ∧ ¬ š‘… ≤ š‘Š ) ) ∧ ( ( š‘ƒ ≠ š‘„ ∧ š‘† ≠ š‘‡ ) ∧ ( ¬ š‘† ≤ ( š‘ƒ ∨ š‘„ ) ∧ ¬ š‘‡ ≤ ( š‘ƒ ∨ š‘„ ) ) ∧ š‘… ≤ ( š‘ƒ ∨ š‘„ ) ) ) → ( š‘Œ ∨ š‘‡ ) = ( š‘‡ ∨ š‘… ) )
36 25 35 oveq12d ⊢ ( ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘ƒ ∈ š“ ∧ ¬ š‘ƒ ≤ š‘Š ) ∧ ( š‘„ ∈ š“ ∧ ¬ š‘„ ≤ š‘Š ) ) ∧ ( ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ∧ ( š‘… ∈ š“ ∧ ¬ š‘… ≤ š‘Š ) ) ∧ ( ( š‘ƒ ≠ š‘„ ∧ š‘† ≠ š‘‡ ) ∧ ( ¬ š‘† ≤ ( š‘ƒ ∨ š‘„ ) ∧ ¬ š‘‡ ≤ ( š‘ƒ ∨ š‘„ ) ) ∧ š‘… ≤ ( š‘ƒ ∨ š‘„ ) ) ) → ( ( š· ∨ š‘† ) ∧ ( š‘Œ ∨ š‘‡ ) ) = ( ( š‘† ∨ š‘… ) ∧ ( š‘‡ ∨ š‘… ) ) )
37 simp12l ⊢ ( ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘ƒ ∈ š“ ∧ ¬ š‘ƒ ≤ š‘Š ) ∧ ( š‘„ ∈ š“ ∧ ¬ š‘„ ≤ š‘Š ) ) ∧ ( ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ∧ ( š‘… ∈ š“ ∧ ¬ š‘… ≤ š‘Š ) ) ∧ ( ( š‘ƒ ≠ š‘„ ∧ š‘† ≠ š‘‡ ) ∧ ( ¬ š‘† ≤ ( š‘ƒ ∨ š‘„ ) ∧ ¬ š‘‡ ≤ ( š‘ƒ ∨ š‘„ ) ) ∧ š‘… ≤ ( š‘ƒ ∨ š‘„ ) ) ) → š‘ƒ ∈ š“ )
38 simp13l ⊢ ( ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘ƒ ∈ š“ ∧ ¬ š‘ƒ ≤ š‘Š ) ∧ ( š‘„ ∈ š“ ∧ ¬ š‘„ ≤ š‘Š ) ) ∧ ( ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ∧ ( š‘… ∈ š“ ∧ ¬ š‘… ≤ š‘Š ) ) ∧ ( ( š‘ƒ ≠ š‘„ ∧ š‘† ≠ š‘‡ ) ∧ ( ¬ š‘† ≤ ( š‘ƒ ∨ š‘„ ) ∧ ¬ š‘‡ ≤ ( š‘ƒ ∨ š‘„ ) ) ∧ š‘… ≤ ( š‘ƒ ∨ š‘„ ) ) ) → š‘„ ∈ š“ )
39 simp21 ⊢ ( ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘ƒ ∈ š“ ∧ ¬ š‘ƒ ≤ š‘Š ) ∧ ( š‘„ ∈ š“ ∧ ¬ š‘„ ≤ š‘Š ) ) ∧ ( ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ∧ ( š‘… ∈ š“ ∧ ¬ š‘… ≤ š‘Š ) ) ∧ ( ( š‘ƒ ≠ š‘„ ∧ š‘† ≠ š‘‡ ) ∧ ( ¬ š‘† ≤ ( š‘ƒ ∨ š‘„ ) ∧ ¬ š‘‡ ≤ ( š‘ƒ ∨ š‘„ ) ) ∧ š‘… ≤ ( š‘ƒ ∨ š‘„ ) ) ) → ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) )
40 1 2 3 4 5 6 7 cdleme1 ⊢ ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘ƒ ∈ š“ ∧ š‘„ ∈ š“ ∧ ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ) ) → ( š‘† ∨ š¹ ) = ( š‘† ∨ š‘ˆ ) )
41 12 13 37 38 39 40 syl23anc ⊢ ( ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘ƒ ∈ š“ ∧ ¬ š‘ƒ ≤ š‘Š ) ∧ ( š‘„ ∈ š“ ∧ ¬ š‘„ ≤ š‘Š ) ) ∧ ( ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ∧ ( š‘… ∈ š“ ∧ ¬ š‘… ≤ š‘Š ) ) ∧ ( ( š‘ƒ ≠ š‘„ ∧ š‘† ≠ š‘‡ ) ∧ ( ¬ š‘† ≤ ( š‘ƒ ∨ š‘„ ) ∧ ¬ š‘‡ ≤ ( š‘ƒ ∨ š‘„ ) ) ∧ š‘… ≤ ( š‘ƒ ∨ š‘„ ) ) ) → ( š‘† ∨ š¹ ) = ( š‘† ∨ š‘ˆ ) )
42 simp22 ⊢ ( ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘ƒ ∈ š“ ∧ ¬ š‘ƒ ≤ š‘Š ) ∧ ( š‘„ ∈ š“ ∧ ¬ š‘„ ≤ š‘Š ) ) ∧ ( ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ∧ ( š‘… ∈ š“ ∧ ¬ š‘… ≤ š‘Š ) ) ∧ ( ( š‘ƒ ≠ š‘„ ∧ š‘† ≠ š‘‡ ) ∧ ( ¬ š‘† ≤ ( š‘ƒ ∨ š‘„ ) ∧ ¬ š‘‡ ≤ ( š‘ƒ ∨ š‘„ ) ) ∧ š‘… ≤ ( š‘ƒ ∨ š‘„ ) ) ) → ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) )
43 1 2 3 4 5 6 8 cdleme1 ⊢ ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘ƒ ∈ š“ ∧ š‘„ ∈ š“ ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ) ) → ( š‘‡ ∨ šŗ ) = ( š‘‡ ∨ š‘ˆ ) )
44 12 13 37 38 42 43 syl23anc ⊢ ( ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘ƒ ∈ š“ ∧ ¬ š‘ƒ ≤ š‘Š ) ∧ ( š‘„ ∈ š“ ∧ ¬ š‘„ ≤ š‘Š ) ) ∧ ( ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ∧ ( š‘… ∈ š“ ∧ ¬ š‘… ≤ š‘Š ) ) ∧ ( ( š‘ƒ ≠ š‘„ ∧ š‘† ≠ š‘‡ ) ∧ ( ¬ š‘† ≤ ( š‘ƒ ∨ š‘„ ) ∧ ¬ š‘‡ ≤ ( š‘ƒ ∨ š‘„ ) ) ∧ š‘… ≤ ( š‘ƒ ∨ š‘„ ) ) ) → ( š‘‡ ∨ šŗ ) = ( š‘‡ ∨ š‘ˆ ) )
45 41 44 oveq12d ⊢ ( ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘ƒ ∈ š“ ∧ ¬ š‘ƒ ≤ š‘Š ) ∧ ( š‘„ ∈ š“ ∧ ¬ š‘„ ≤ š‘Š ) ) ∧ ( ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ∧ ( š‘… ∈ š“ ∧ ¬ š‘… ≤ š‘Š ) ) ∧ ( ( š‘ƒ ≠ š‘„ ∧ š‘† ≠ š‘‡ ) ∧ ( ¬ š‘† ≤ ( š‘ƒ ∨ š‘„ ) ∧ ¬ š‘‡ ≤ ( š‘ƒ ∨ š‘„ ) ) ∧ š‘… ≤ ( š‘ƒ ∨ š‘„ ) ) ) → ( ( š‘† ∨ š¹ ) ∧ ( š‘‡ ∨ šŗ ) ) = ( ( š‘† ∨ š‘ˆ ) ∧ ( š‘‡ ∨ š‘ˆ ) ) )
46 36 45 oveq12d ⊢ ( ( ( ( š¾ ∈ HL ∧ š‘Š ∈ š» ) ∧ ( š‘ƒ ∈ š“ ∧ ¬ š‘ƒ ≤ š‘Š ) ∧ ( š‘„ ∈ š“ ∧ ¬ š‘„ ≤ š‘Š ) ) ∧ ( ( š‘† ∈ š“ ∧ ¬ š‘† ≤ š‘Š ) ∧ ( š‘‡ ∈ š“ ∧ ¬ š‘‡ ≤ š‘Š ) ∧ ( š‘… ∈ š“ ∧ ¬ š‘… ≤ š‘Š ) ) ∧ ( ( š‘ƒ ≠ š‘„ ∧ š‘† ≠ š‘‡ ) ∧ ( ¬ š‘† ≤ ( š‘ƒ ∨ š‘„ ) ∧ ¬ š‘‡ ≤ ( š‘ƒ ∨ š‘„ ) ) ∧ š‘… ≤ ( š‘ƒ ∨ š‘„ ) ) ) → ( ( ( š· ∨ š‘† ) ∧ ( š‘Œ ∨ š‘‡ ) ) ∨ ( ( š‘† ∨ š¹ ) ∧ ( š‘‡ ∨ šŗ ) ) ) = ( ( ( š‘† ∨ š‘… ) ∧ ( š‘‡ ∨ š‘… ) ) ∨ ( ( š‘† ∨ š‘ˆ ) ∧ ( š‘‡ ∨ š‘ˆ ) ) ) )