cdleme21e

Description: Part of proof of Lemma E in Crawley p. 113, last paragraph on p. 115, 3rd line. Y , G , O , E , B , Z represent s_2, f(s), f_s(r), z_2, f(z), f_z(r) respectively. We prove that if u <_ s \/ z, then f_t(r) = f_z(r). (Contributed by NM, 29-Nov-2012)

	Ref	Expression
Hypotheses	cdleme21.l	⊢ ≤ = ( le ‘ 𝐾 )
	cdleme21.j	⊢ ∨ = ( join ‘ 𝐾 )
	cdleme21.m	⊢ ∧ = ( meet ‘ 𝐾 )
	cdleme21.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	cdleme21.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	cdleme21.u	⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
	cdleme21.f	⊢ 𝐹 = ( ( 𝑆 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) )
	cdleme21.b	⊢ 𝐵 = ( ( 𝑧 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) )
	cdleme21.d	⊢ 𝐷 = ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 )
	cdleme21.e	⊢ 𝐸 = ( ( 𝑅 ∨ 𝑧 ) ∧ 𝑊 )
	cdleme21d.n	⊢ 𝑁 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ∨ 𝐷 ) )
	cdleme21d.z	⊢ 𝑍 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐵 ∨ 𝐸 ) )
	cdleme21.g	⊢ 𝐺 = ( ( 𝑇 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑇 ) ∧ 𝑊 ) ) )
	cdleme21.y	⊢ 𝑌 = ( ( 𝑅 ∨ 𝑇 ) ∧ 𝑊 )
	cdleme21.o	⊢ 𝑂 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐺 ∨ 𝑌 ) )
Assertion	cdleme21e	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → 𝑂 = 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		cdleme21.l	⊢ ≤ = ( le ‘ 𝐾 )
2		cdleme21.j	⊢ ∨ = ( join ‘ 𝐾 )
3		cdleme21.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		cdleme21.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		cdleme21.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6		cdleme21.u	⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
7		cdleme21.f	⊢ 𝐹 = ( ( 𝑆 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) )
8		cdleme21.b	⊢ 𝐵 = ( ( 𝑧 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) )
9		cdleme21.d	⊢ 𝐷 = ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 )
10		cdleme21.e	⊢ 𝐸 = ( ( 𝑅 ∨ 𝑧 ) ∧ 𝑊 )
11		cdleme21d.n	⊢ 𝑁 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ∨ 𝐷 ) )
12		cdleme21d.z	⊢ 𝑍 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐵 ∨ 𝐸 ) )
13		cdleme21.g	⊢ 𝐺 = ( ( 𝑇 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑇 ) ∧ 𝑊 ) ) )
14		cdleme21.y	⊢ 𝑌 = ( ( 𝑅 ∨ 𝑇 ) ∧ 𝑊 )
15		cdleme21.o	⊢ 𝑂 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐺 ∨ 𝑌 ) )
16		simp11	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
17		simp12	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
18		simp13	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
19		simp31	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) )
20		simp22	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) )
21		simp33l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) )
22		simp231	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → 𝑃 ≠ 𝑄 )
23		simp13l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → 𝑄 ∈ 𝐴 )
24		simp21l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → 𝑆 ∈ 𝐴 )
25		simp232	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) )
26	24 22 25	3jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → ( 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) )
27		simp32r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) )
28	21	simpld	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → 𝑧 ∈ 𝐴 )
29		simp33r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) )
30	1 2 3 4 5 6	cdleme21at	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) → 𝑇 ≠ 𝑧 )
31	16 17 23 26 27 28 29 30	syl322anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → 𝑇 ≠ 𝑧 )
32	22 31	jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → ( 𝑃 ≠ 𝑄 ∧ 𝑇 ≠ 𝑧 ) )
33		simp233	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) )
34		simp11l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → 𝐾 ∈ HL )
35		simp12l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → 𝑃 ∈ 𝐴 )
36	1 2 4	cdleme21b	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) → ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) )
37	34 35 23 24 22 25 28 29 36	syl332anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) )
38		simp32l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) )
39	33 37 38	3jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → ( ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) )
40		simp21	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) )
41	22 25 27	3jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) )
42	1 2 3 4 5 6	cdleme21ct	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) → ¬ 𝑈 ≤ ( 𝑇 ∨ 𝑧 ) )
43	16 17 23 40 20 41 21 29 42	syl332anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → ¬ 𝑈 ≤ ( 𝑇 ∨ 𝑧 ) )
44		eqid	⊢ ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 ) = ( ( 𝑇 ∨ 𝑧 ) ∧ 𝑊 )
45	1 2 3 4 5 6 13 8 14 10 44 15 12	cdleme20	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑇 ≠ 𝑧 ) ∧ ( ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑈 ≤ ( 𝑇 ∨ 𝑧 ) ) ) → 𝑂 = 𝑍 )
46	16 17 18 19 20 21 32 39 43 45	syl333anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → 𝑂 = 𝑍 )

Metamath Proof Explorer

Theorem cdleme21e

Proof