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 41099

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 40402	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ^◡𝐹 ∈ 𝑇)
8	2, 4, 7	syl2anc 584	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ^◡𝐹 ∈ 𝑇)
9	5, 6	ltrnco 40975	. . . . . . 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 40440	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∘ ^◡𝐹) ∈ 𝑇) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ≤ 𝑊)
14	2, 10, 13	syl2anc 584	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ≤ 𝑊)
15		simp23 1209	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑋 ∈ 𝑇)
16	5, 6	ltrnco 40975	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑇 ∧ ^◡𝐹 ∈ 𝑇) → (𝑋 ∘ ^◡𝐹) ∈ 𝑇)
17	2, 15, 8, 16	syl3anc 1373	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋 ∘ ^◡𝐹) ∈ 𝑇)
18	11, 5, 6, 12	trlle 40440	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∘ ^◡𝐹) ∈ 𝑇) → (𝑅‘(𝑋 ∘ ^◡𝐹)) ≤ 𝑊)
19	2, 17, 18	syl2anc 584	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘(𝑋 ∘ ^◡𝐹)) ≤ 𝑊)
20		simp1l 1198	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ HL)
21	20	hllatd 39620	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ Lat)
22		cdlemk.b	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝐾)
23	22, 5, 6, 12	trlcl 40420	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∘ ^◡𝐹) ∈ 𝑇) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐵)
24	2, 10, 23	syl2anc 584	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐵)
25	22, 5, 6, 12	trlcl 40420	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∘ ^◡𝐹) ∈ 𝑇) → (𝑅‘(𝑋 ∘ ^◡𝐹)) ∈ 𝐵)
26	2, 17, 25	syl2anc 584	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘(𝑋 ∘ ^◡𝐹)) ∈ 𝐵)
27		simp1r 1199	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ 𝐻)
28	22, 5	lhpbase 40254	. . . . . . 7 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)
29	27, 28	syl 17	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ 𝐵)
30		cdlemk.j	. . . . . . 7 ⊢ ∨ = (join‘𝐾)
31	22, 11, 30	latjle12 18373	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ ((𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐵 ∧ (𝑅‘(𝑋 ∘ ^◡𝐹)) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → (((𝑅‘(𝐺 ∘ ^◡𝐹)) ≤ 𝑊 ∧ (𝑅‘(𝑋 ∘ ^◡𝐹)) ≤ 𝑊) ↔ ((𝑅‘(𝐺 ∘ ^◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ^◡𝐹))) ≤ 𝑊))
32	21, 24, 26, 29, 31	syl13anc 1374	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝑅‘(𝐺 ∘ ^◡𝐹)) ≤ 𝑊 ∧ (𝑅‘(𝑋 ∘ ^◡𝐹)) ≤ 𝑊) ↔ ((𝑅‘(𝐺 ∘ ^◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ^◡𝐹))) ≤ 𝑊))
33	14, 19, 32	mpbi2and 712	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑅‘(𝐺 ∘ ^◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ^◡𝐹))) ≤ 𝑊)
34	22, 30	latjcl 18362	. . . . . 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 40396	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝐺‘𝑃) ∈ 𝐴)
39	2, 3, 36, 38	syl3anc 1373	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐺‘𝑃) ∈ 𝐴)
40	11, 37, 5, 6	ltrnat 40396	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝑋‘𝑃) ∈ 𝐴)
41	2, 15, 36, 40	syl3anc 1373	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋‘𝑃) ∈ 𝐴)
42	22, 30, 37	hlatjcl 39623	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝐺‘𝑃) ∈ 𝐴 ∧ (𝑋‘𝑃) ∈ 𝐴) → ((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∈ 𝐵)
43	20, 39, 41, 42	syl3anc 1373	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∈ 𝐵)
44		cdlemk.m	. . . . . 6 ⊢ ∧ = (meet‘𝐾)
45	22, 11, 44	latmlem2 18393	. . . . 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 41095	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ 𝑊) = (𝑅‘(𝑋 ∘ ^◡𝐺)))
50	20, 27, 3, 15, 48, 49	syl221anc 1383	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ 𝑊) = (𝑅‘(𝑋 ∘ ^◡𝐺)))
51	47, 50	breqtrd 5124	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑅‘(𝐺 ∘ ^◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ^◡𝐹)))) ≤ (𝑅‘(𝑋 ∘ ^◡𝐺)))
52	1, 51	eqbrtrid 5133	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑉 ≤ (𝑅‘(𝑋 ∘ ^◡𝐺)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 class class class wbr 5098 ^◡ccnv 5623 ∘ ccom 5628 ‘cfv 6492 (class class class)co 7358 Basecbs 17136 lecple 17184 joincjn 18234 meetcmee 18235 Latclat 18354 Atomscatm 39519 HLchlt 39606 LHypclh 40240 LTrncltrn 40357 trLctrl 40414

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-riotaBAD 39209

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-iun 4948 df-iin 4949 df-br 5099 df-opab 5161 df-mpt 5180 df-id 5519 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-1st 7933 df-2nd 7934 df-undef 8215 df-map 8765 df-proset 18217 df-poset 18236 df-plt 18251 df-lub 18267 df-glb 18268 df-join 18269 df-meet 18270 df-p0 18346 df-p1 18347 df-lat 18355 df-clat 18422 df-oposet 39432 df-ol 39434 df-oml 39435 df-covers 39522 df-ats 39523 df-atl 39554 df-cvlat 39578 df-hlat 39607 df-llines 39754 df-lplanes 39755 df-lvols 39756 df-lines 39757 df-psubsp 39759 df-pmap 39760 df-padd 40052 df-lhyp 40244 df-laut 40245 df-ldil 40360 df-ltrn 40361 df-trl 40415

This theorem is referenced by: cdlemk11 41105 cdlemk11u 41127

W3C validator