cdlemk10 - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > cdlemk10		Structured version Visualization version GIF version

Theorem cdlemk10 40862

Description: Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 29-Jun-2013.)

**Hypotheses**
Ref	Expression
cdlemk.b	⊢ 𝐵 = (Base‘𝐾)
cdlemk.l	⊢ ≤ = (le‘𝐾)
cdlemk.j	⊢ ∨ = (join‘𝐾)
cdlemk.a	⊢ 𝐴 = (Atoms‘𝐾)
cdlemk.h	⊢ 𝐻 = (LHyp‘𝐾)
cdlemk.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
cdlemk.r	⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
cdlemk.m	⊢ ∧ = (meet‘𝐾)
cdlemk.v1	⊢ 𝑉 = (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑅‘(𝐺 ∘ ^◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ^◡𝐹))))

**Assertion**
Ref	Expression
cdlemk10	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑉 ≤ (𝑅‘(𝑋 ∘ ^◡𝐺)))

**Proof of Theorem cdlemk10**
Step	Hyp	Ref	Expression
1		cdlemk.v1	. 2 ⊢ 𝑉 = (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑅‘(𝐺 ∘ ^◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ^◡𝐹))))
2		simp1 1136	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
3		simp22 1208	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐺 ∈ 𝑇)
4		simp21 1207	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐹 ∈ 𝑇)
5		cdlemk.h	. . . . . . . . 9 ⊢ 𝐻 = (LHyp‘𝐾)
6		cdlemk.t	. . . . . . . . 9 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
7	5, 6	ltrncnv 40165	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ^◡𝐹 ∈ 𝑇)
8	2, 4, 7	syl2anc 584	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ^◡𝐹 ∈ 𝑇)
9	5, 6	ltrnco 40738	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ ^◡𝐹 ∈ 𝑇) → (𝐺 ∘ ^◡𝐹) ∈ 𝑇)
10	2, 3, 8, 9	syl3anc 1373	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐺 ∘ ^◡𝐹) ∈ 𝑇)
11		cdlemk.l	. . . . . . 7 ⊢ ≤ = (le‘𝐾)
12		cdlemk.r	. . . . . . 7 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
13	11, 5, 6, 12	trlle 40203	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∘ ^◡𝐹) ∈ 𝑇) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ≤ 𝑊)
14	2, 10, 13	syl2anc 584	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ≤ 𝑊)
15		simp23 1209	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑋 ∈ 𝑇)
16	5, 6	ltrnco 40738	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑇 ∧ ^◡𝐹 ∈ 𝑇) → (𝑋 ∘ ^◡𝐹) ∈ 𝑇)
17	2, 15, 8, 16	syl3anc 1373	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋 ∘ ^◡𝐹) ∈ 𝑇)
18	11, 5, 6, 12	trlle 40203	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∘ ^◡𝐹) ∈ 𝑇) → (𝑅‘(𝑋 ∘ ^◡𝐹)) ≤ 𝑊)
19	2, 17, 18	syl2anc 584	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘(𝑋 ∘ ^◡𝐹)) ≤ 𝑊)
20		simp1l 1198	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ HL)
21	20	hllatd 39382	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ Lat)
22		cdlemk.b	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝐾)
23	22, 5, 6, 12	trlcl 40183	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∘ ^◡𝐹) ∈ 𝑇) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐵)
24	2, 10, 23	syl2anc 584	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐵)
25	22, 5, 6, 12	trlcl 40183	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∘ ^◡𝐹) ∈ 𝑇) → (𝑅‘(𝑋 ∘ ^◡𝐹)) ∈ 𝐵)
26	2, 17, 25	syl2anc 584	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘(𝑋 ∘ ^◡𝐹)) ∈ 𝐵)
27		simp1r 1199	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ 𝐻)
28	22, 5	lhpbase 40017	. . . . . . 7 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)
29	27, 28	syl 17	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ 𝐵)
30		cdlemk.j	. . . . . . 7 ⊢ ∨ = (join‘𝐾)
31	22, 11, 30	latjle12 18460	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ ((𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐵 ∧ (𝑅‘(𝑋 ∘ ^◡𝐹)) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → (((𝑅‘(𝐺 ∘ ^◡𝐹)) ≤ 𝑊 ∧ (𝑅‘(𝑋 ∘ ^◡𝐹)) ≤ 𝑊) ↔ ((𝑅‘(𝐺 ∘ ^◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ^◡𝐹))) ≤ 𝑊))
32	21, 24, 26, 29, 31	syl13anc 1374	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝑅‘(𝐺 ∘ ^◡𝐹)) ≤ 𝑊 ∧ (𝑅‘(𝑋 ∘ ^◡𝐹)) ≤ 𝑊) ↔ ((𝑅‘(𝐺 ∘ ^◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ^◡𝐹))) ≤ 𝑊))
33	14, 19, 32	mpbi2and 712	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑅‘(𝐺 ∘ ^◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ^◡𝐹))) ≤ 𝑊)
34	22, 30	latjcl 18449	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐵 ∧ (𝑅‘(𝑋 ∘ ^◡𝐹)) ∈ 𝐵) → ((𝑅‘(𝐺 ∘ ^◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ^◡𝐹))) ∈ 𝐵)
35	21, 24, 26, 34	syl3anc 1373	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑅‘(𝐺 ∘ ^◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ^◡𝐹))) ∈ 𝐵)
36		simp3l 1202	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑃 ∈ 𝐴)
37		cdlemk.a	. . . . . . . 8 ⊢ 𝐴 = (Atoms‘𝐾)
38	11, 37, 5, 6	ltrnat 40159	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝐺‘𝑃) ∈ 𝐴)
39	2, 3, 36, 38	syl3anc 1373	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐺‘𝑃) ∈ 𝐴)
40	11, 37, 5, 6	ltrnat 40159	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝑋‘𝑃) ∈ 𝐴)
41	2, 15, 36, 40	syl3anc 1373	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋‘𝑃) ∈ 𝐴)
42	22, 30, 37	hlatjcl 39385	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝐺‘𝑃) ∈ 𝐴 ∧ (𝑋‘𝑃) ∈ 𝐴) → ((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∈ 𝐵)
43	20, 39, 41, 42	syl3anc 1373	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∈ 𝐵)
44		cdlemk.m	. . . . . 6 ⊢ ∧ = (meet‘𝐾)
45	22, 11, 44	latmlem2 18480	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (((𝑅‘(𝐺 ∘ ^◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ^◡𝐹))) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ ((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∈ 𝐵)) → (((𝑅‘(𝐺 ∘ ^◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ^◡𝐹))) ≤ 𝑊 → (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑅‘(𝐺 ∘ ^◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ^◡𝐹)))) ≤ (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ 𝑊)))
46	21, 35, 29, 43, 45	syl13anc 1374	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝑅‘(𝐺 ∘ ^◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ^◡𝐹))) ≤ 𝑊 → (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑅‘(𝐺 ∘ ^◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ^◡𝐹)))) ≤ (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ 𝑊)))
47	33, 46	mpd 15	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑅‘(𝐺 ∘ ^◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ^◡𝐹)))) ≤ (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ 𝑊))
48		simp3 1138	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
49	22, 11, 30, 37, 5, 6, 12, 44	cdlemk9 40858	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ 𝑊) = (𝑅‘(𝑋 ∘ ^◡𝐺)))
50	20, 27, 3, 15, 48, 49	syl221anc 1383	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ 𝑊) = (𝑅‘(𝑋 ∘ ^◡𝐺)))
51	47, 50	breqtrd 5145	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑅‘(𝐺 ∘ ^◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ^◡𝐹)))) ≤ (𝑅‘(𝑋 ∘ ^◡𝐺)))
52	1, 51	eqbrtrid 5154	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑉 ≤ (𝑅‘(𝑋 ∘ ^◡𝐺)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2108 class class class wbr 5119 ^◡ccnv 5653 ∘ ccom 5658 ‘cfv 6531 (class class class)co 7405 Basecbs 17228 lecple 17278 joincjn 18323 meetcmee 18324 Latclat 18441 Atomscatm 39281 HLchlt 39368 LHypclh 40003 LTrncltrn 40120 trLctrl 40177

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-rep 5249 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7729 ax-riotaBAD 38971

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3061 df-rmo 3359 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-op 4608 df-uni 4884 df-iun 4969 df-iin 4970 df-br 5120 df-opab 5182 df-mpt 5202 df-id 5548 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-iota 6484 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7362 df-ov 7408 df-oprab 7409 df-mpo 7410 df-1st 7988 df-2nd 7989 df-undef 8272 df-map 8842 df-proset 18306 df-poset 18325 df-plt 18340 df-lub 18356 df-glb 18357 df-join 18358 df-meet 18359 df-p0 18435 df-p1 18436 df-lat 18442 df-clat 18509 df-oposet 39194 df-ol 39196 df-oml 39197 df-covers 39284 df-ats 39285 df-atl 39316 df-cvlat 39340 df-hlat 39369 df-llines 39517 df-lplanes 39518 df-lvols 39519 df-lines 39520 df-psubsp 39522 df-pmap 39523 df-padd 39815 df-lhyp 40007 df-laut 40008 df-ldil 40123 df-ltrn 40124 df-trl 40178

This theorem is referenced by: cdlemk11 40868 cdlemk11u 40890

W3C validator