Theorem cdleme15d 38288

Description: Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, showing, in their notation, s₁ ∨ t₁ ≤ w. 𝐶 and 𝑋 represent s₁ and t₁ respectively. The order of our operations is slightly different. (Contributed by NM, 10-Oct-2012.)

Hypotheses

Ref	Expression
cdleme12.l	⊢ ≤ = (le‘𝐾)
cdleme12.j	⊢ ∨ = (join‘𝐾)
cdleme12.m	⊢ ∧ = (meet‘𝐾)
cdleme12.a	⊢ 𝐴 = (Atoms‘𝐾)
cdleme12.h	⊢ 𝐻 = (LHyp‘𝐾)
cdleme12.u	⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)
cdleme12.f	⊢ 𝐹 = ((𝑆 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊)))
cdleme12.g	⊢ 𝐺 = ((𝑇 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑇) ∧ 𝑊)))
cdleme15.c	⊢ 𝐶 = ((𝑃 ∨ 𝑆) ∧ 𝑊)
cdleme15.x	⊢ 𝑋 = ((𝑃 ∨ 𝑇) ∧ 𝑊)

Assertion

Ref	Expression
cdleme15d	⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇)) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) → (𝑋 ∨ 𝐶) ≤ 𝑊)

Proof of Theorem cdleme15d

Step	Hyp	Ref	Expression
1		cdleme15.x	. . 3 ⊢ 𝑋 = ((𝑃 ∨ 𝑇) ∧ 𝑊)
2		simp11l 1283	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇)) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) → 𝐾 ∈ HL)
3	2	hllatd 37375	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇)) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) → 𝐾 ∈ Lat)
4		simp12l 1285	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇)) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) → 𝑃 ∈ 𝐴)
5		simp22l 1291	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇)) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) → 𝑇 ∈ 𝐴)
6		eqid 2738	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
7		cdleme12.j	. . . . . 6 ⊢ ∨ = (join‘𝐾)
8		cdleme12.a	. . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾)
9	6, 7, 8	hlatjcl 37378	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (𝑃 ∨ 𝑇) ∈ (Base‘𝐾))
10	2, 4, 5, 9	syl3anc 1370	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇)) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) → (𝑃 ∨ 𝑇) ∈ (Base‘𝐾))
11		simp11r 1284	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇)) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) → 𝑊 ∈ 𝐻)
12		cdleme12.h	. . . . . 6 ⊢ 𝐻 = (LHyp‘𝐾)
13	6, 12	lhpbase 38009	. . . . 5 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾))
14	11, 13	syl 17	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇)) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) → 𝑊 ∈ (Base‘𝐾))
15		cdleme12.l	. . . . 5 ⊢ ≤ = (le‘𝐾)
16		cdleme12.m	. . . . 5 ⊢ ∧ = (meet‘𝐾)
17	6, 15, 16	latmle2 18181	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑇) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑇) ∧ 𝑊) ≤ 𝑊)
18	3, 10, 14, 17	syl3anc 1370	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇)) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) → ((𝑃 ∨ 𝑇) ∧ 𝑊) ≤ 𝑊)
19	1, 18	eqbrtrid 5111	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇)) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) → 𝑋 ≤ 𝑊)
20		cdleme15.c	. . 3 ⊢ 𝐶 = ((𝑃 ∨ 𝑆) ∧ 𝑊)
21		simp21l 1289	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇)) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) → 𝑆 ∈ 𝐴)
22	6, 7, 8	hlatjcl 37378	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) → (𝑃 ∨ 𝑆) ∈ (Base‘𝐾))
23	2, 4, 21, 22	syl3anc 1370	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇)) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) → (𝑃 ∨ 𝑆) ∈ (Base‘𝐾))
24	6, 15, 16	latmle2 18181	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑆) ∧ 𝑊) ≤ 𝑊)
25	3, 23, 14, 24	syl3anc 1370	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇)) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) → ((𝑃 ∨ 𝑆) ∧ 𝑊) ≤ 𝑊)
26	20, 25	eqbrtrid 5111	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇)) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) → 𝐶 ≤ 𝑊)
27	6, 16	latmcl 18156	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑇) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑇) ∧ 𝑊) ∈ (Base‘𝐾))
28	3, 10, 14, 27	syl3anc 1370	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇)) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) → ((𝑃 ∨ 𝑇) ∧ 𝑊) ∈ (Base‘𝐾))
29	1, 28	eqeltrid 2843	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇)) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) → 𝑋 ∈ (Base‘𝐾))
30	6, 16	latmcl 18156	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑆) ∧ 𝑊) ∈ (Base‘𝐾))
31	3, 23, 14, 30	syl3anc 1370	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇)) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) → ((𝑃 ∨ 𝑆) ∧ 𝑊) ∈ (Base‘𝐾))
32	20, 31	eqeltrid 2843	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇)) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) → 𝐶 ∈ (Base‘𝐾))
33	6, 15, 7	latjle12 18166	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ (Base‘𝐾) ∧ 𝐶 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑋 ≤ 𝑊 ∧ 𝐶 ≤ 𝑊) ↔ (𝑋 ∨ 𝐶) ≤ 𝑊))
34	3, 29, 32, 14, 33	syl13anc 1371	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇)) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) → ((𝑋 ≤ 𝑊 ∧ 𝐶 ≤ 𝑊) ↔ (𝑋 ∨ 𝐶) ≤ 𝑊))
35	19, 26, 34	mpbi2and 709	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇)) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) → (𝑋 ∨ 𝐶) ≤ 𝑊)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1086   = wceq 1539   ∈ wcel 2106   ≠ wne 2943   class class class wbr 5076  ‘cfv 6435  (class class class)co 7277  Basecbs 16910  lecple 16967  joincjn 18027  meetcmee 18028  Latclat 18147  Atomscatm 37274  HLchlt 37361  LHypclh 37995

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5211  ax-sep 5225  ax-nul 5232  ax-pow 5290  ax-pr 5354  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3433  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4259  df-if 4462  df-pw 4537  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4842  df-iun 4928  df-br 5077  df-opab 5139  df-mpt 5160  df-id 5491  df-xp 5597  df-rel 5598  df-cnv 5599  df-co 5600  df-dm 5601  df-rn 5602  df-res 5603  df-ima 5604  df-iota 6393  df-fun 6437  df-fn 6438  df-f 6439  df-f1 6440  df-fo 6441  df-f1o 6442  df-fv 6443  df-riota 7234  df-ov 7280  df-oprab 7281  df-poset 18029  df-lub 18062  df-glb 18063  df-join 18064  df-meet 18065  df-lat 18148  df-ats 37278  df-atl 37309  df-cvlat 37333  df-hlat 37362  df-lhyp 37999

This theorem is referenced by:  cdleme15  38289