Metamath Proof Explorer

Theorem cdleme36m

Description: Part of proof of Lemma E in Crawley p. 113. Show that f(x) is one-to-one on P .\/ Q line. TODO: FIX COMMENT. (Contributed by NM, 11-Mar-2013)

Ref Expression
Hypotheses cdleme36.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cdleme36.l ⊢ ≤ = ( le ‘ 𝐾 )
cdleme36.j ⊢ ∨ = ( join ‘ 𝐾 )
cdleme36.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdleme36.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdleme36.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdleme36.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
cdleme36.e ⊢ 𝐸 = ( ( 𝑡 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑡 ) ∧ 𝑊 ) ) )
cdleme36.v ⊢ 𝑉 = ( ( 𝑡 ∨ 𝐸 ) ∧ 𝑊 )
cdleme36.f ⊢ 𝐹 = ( ( 𝑅 ∨ 𝑉 ) ∧ ( 𝐸 ∨ ( ( 𝑡 ∨ 𝑅 ) ∧ 𝑊 ) ) )
cdleme36.c ⊢ 𝐶 = ( ( 𝑆 ∨ 𝑉 ) ∧ ( 𝐸 ∨ ( ( 𝑡 ∨ 𝑆 ) ∧ 𝑊 ) ) )
Assertion cdleme36m ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝐹 = 𝐶 ) ∧ ( ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝑅 = 𝑆 )

Proof

Step Hyp Ref Expression
1 cdleme36.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cdleme36.l ⊢ ≤ = ( le ‘ 𝐾 )
3 cdleme36.j ⊢ ∨ = ( join ‘ 𝐾 )
4 cdleme36.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 cdleme36.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 cdleme36.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7 cdleme36.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
8 cdleme36.e ⊢ 𝐸 = ( ( 𝑡 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑡 ) ∧ 𝑊 ) ) )
9 cdleme36.v ⊢ 𝑉 = ( ( 𝑡 ∨ 𝐸 ) ∧ 𝑊 )
10 cdleme36.f ⊢ 𝐹 = ( ( 𝑅 ∨ 𝑉 ) ∧ ( 𝐸 ∨ ( ( 𝑡 ∨ 𝑅 ) ∧ 𝑊 ) ) )
11 cdleme36.c ⊢ 𝐶 = ( ( 𝑆 ∨ 𝑉 ) ∧ ( 𝐸 ∨ ( ( 𝑡 ∨ 𝑆 ) ∧ 𝑊 ) ) )
12 simp11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝐹 = 𝐶 ) ∧ ( ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13 simp3rl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝐹 = 𝐶 ) ∧ ( ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) )
14 simp12 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝐹 = 𝐶 ) ∧ ( ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
15 simp13 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝐹 = 𝐶 ) ∧ ( ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
16 simp21 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝐹 = 𝐶 ) ∧ ( ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝑃 ≠ 𝑄 )
17 simp3rr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝐹 = 𝐶 ) ∧ ( ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) )
18 2 3 4 5 6 7 8 cdleme3fa ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐸 ∈ 𝐴 )
19 12 14 15 13 16 17 18 syl132anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝐹 = 𝐶 ) ∧ ( ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝐸 ∈ 𝐴 )
20 2 3 4 5 6 7 8 cdleme3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ¬ 𝐸 ≤ 𝑊 )
21 12 14 15 13 16 17 20 syl132anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝐹 = 𝐶 ) ∧ ( ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ¬ 𝐸 ≤ 𝑊 )
22 19 21 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝐹 = 𝐶 ) ∧ ( ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( 𝐸 ∈ 𝐴 ∧ ¬ 𝐸 ≤ 𝑊 ) )
23 simp13l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝐹 = 𝐶 ) ∧ ( ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝑄 ∈ 𝐴 )
24 23 16 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝐹 = 𝐶 ) ∧ ( ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) )
25 2 3 4 5 6 7 8 cdleme3b ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ) ) → 𝐸 ≠ 𝑡 )
26 12 14 24 13 25 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝐹 = 𝐶 ) ∧ ( ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝐸 ≠ 𝑡 )
27 26 necomd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝐹 = 𝐶 ) ∧ ( ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝑡 ≠ 𝐸 )
28 simp22 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝐹 = 𝐶 ) ∧ ( ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) )
29 simp23 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝐹 = 𝐶 ) ∧ ( ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) )
30 simp3l1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝐹 = 𝐶 ) ∧ ( ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) )
31 simp3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝐹 = 𝐶 ) ∧ ( ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) )
32 1 2 3 4 5 6 7 8 cdleme36a ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ¬ 𝑅 ≤ ( 𝑡 ∨ 𝐸 ) )
33 12 14 23 16 28 30 31 32 syl331anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝐹 = 𝐶 ) ∧ ( ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ¬ 𝑅 ≤ ( 𝑡 ∨ 𝐸 ) )
34 simp3l2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝐹 = 𝐶 ) ∧ ( ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) )
35 1 2 3 4 5 6 7 8 cdleme36a ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ¬ 𝑆 ≤ ( 𝑡 ∨ 𝐸 ) )
36 12 14 23 16 29 34 31 35 syl331anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝐹 = 𝐶 ) ∧ ( ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ¬ 𝑆 ≤ ( 𝑡 ∨ 𝐸 ) )
37 simp3l3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝐹 = 𝐶 ) ∧ ( ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝐹 = 𝐶 )
38 2 3 4 5 6 9 10 11 cdleme35h ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ∧ ( 𝐸 ∈ 𝐴 ∧ ¬ 𝐸 ≤ 𝑊 ) ) ∧ ( 𝑡 ≠ 𝐸 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( ¬ 𝑅 ≤ ( 𝑡 ∨ 𝐸 ) ∧ ¬ 𝑆 ≤ ( 𝑡 ∨ 𝐸 ) ∧ 𝐹 = 𝐶 ) ) → 𝑅 = 𝑆 )
39 12 13 22 27 28 29 33 36 37 38 syl333anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝐹 = 𝐶 ) ∧ ( ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝑅 = 𝑆 )