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

Theorem cdlemk15 38170
 Description: Part of proof of Lemma K of [Crawley] p. 118. Line 21 on p. 119. 𝑂, 𝐷 are k1, f1. (Contributed by NM, 1-Jul-2013.)
Hypotheses
Ref Expression
cdlemk1.b 𝐵 = (Base‘𝐾)
cdlemk1.l = (le‘𝐾)
cdlemk1.j = (join‘𝐾)
cdlemk1.m = (meet‘𝐾)
cdlemk1.a 𝐴 = (Atoms‘𝐾)
cdlemk1.h 𝐻 = (LHyp‘𝐾)
cdlemk1.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
cdlemk1.r 𝑅 = ((trL‘𝐾)‘𝑊)
cdlemk1.s 𝑆 = (𝑓𝑇 ↦ (𝑖𝑇 (𝑖𝑃) = ((𝑃 (𝑅𝑓)) ((𝑁𝑃) (𝑅‘(𝑓𝐹))))))
cdlemk1.o 𝑂 = (𝑆𝐷)
Assertion
Ref Expression
cdlemk15 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ (𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐷) ≠ (𝑅𝐹))) → (𝑁𝑃) ((𝑃 (𝑅𝐹)) ((𝑂𝑃) (𝑅‘(𝐹𝐷)))))
Distinct variable groups:   𝑓,𝑖,   ,𝑖   ,𝑓,𝑖   𝐴,𝑖   𝐷,𝑓,𝑖   𝑓,𝐹,𝑖   𝑖,𝐻   𝑖,𝐾   𝑓,𝑁,𝑖   𝑃,𝑓,𝑖   𝑅,𝑓,𝑖   𝑇,𝑓,𝑖   𝑓,𝑊,𝑖
Allowed substitution hints:   𝐴(𝑓)   𝐵(𝑓,𝑖)   𝑆(𝑓,𝑖)   𝐻(𝑓)   𝐾(𝑓)   (𝑓)   𝑂(𝑓,𝑖)

Proof of Theorem cdlemk15
StepHypRef Expression
1 simp11l 1281 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ (𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐷) ≠ (𝑅𝐹))) → 𝐾 ∈ HL)
2 simp22l 1289 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ (𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐷) ≠ (𝑅𝐹))) → 𝑃𝐴)
3 simp11 1200 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ (𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐷) ≠ (𝑅𝐹))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
4 simp21 1203 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ (𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐷) ≠ (𝑅𝐹))) → 𝑁𝑇)
5 cdlemk1.l . . . . . 6 = (le‘𝐾)
6 cdlemk1.a . . . . . 6 𝐴 = (Atoms‘𝐾)
7 cdlemk1.h . . . . . 6 𝐻 = (LHyp‘𝐾)
8 cdlemk1.t . . . . . 6 𝑇 = ((LTrn‘𝐾)‘𝑊)
95, 6, 7, 8ltrnat 37455 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑁𝑇𝑃𝐴) → (𝑁𝑃) ∈ 𝐴)
103, 4, 2, 9syl3anc 1368 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ (𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐷) ≠ (𝑅𝐹))) → (𝑁𝑃) ∈ 𝐴)
11 cdlemk1.j . . . . 5 = (join‘𝐾)
125, 11, 6hlatlej2 36691 . . . 4 ((𝐾 ∈ HL ∧ 𝑃𝐴 ∧ (𝑁𝑃) ∈ 𝐴) → (𝑁𝑃) (𝑃 (𝑁𝑃)))
131, 2, 10, 12syl3anc 1368 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ (𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐷) ≠ (𝑅𝐹))) → (𝑁𝑃) (𝑃 (𝑁𝑃)))
14 simp23 1205 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ (𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐷) ≠ (𝑅𝐹))) → (𝑅𝐹) = (𝑅𝑁))
1514oveq2d 7152 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ (𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐷) ≠ (𝑅𝐹))) → (𝑃 (𝑅𝐹)) = (𝑃 (𝑅𝑁)))
16 simp22 1204 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ (𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐷) ≠ (𝑅𝐹))) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
17 cdlemk1.r . . . . . 6 𝑅 = ((trL‘𝐾)‘𝑊)
185, 11, 6, 7, 8, 17trljat1 37481 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 (𝑅𝑁)) = (𝑃 (𝑁𝑃)))
193, 4, 16, 18syl3anc 1368 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ (𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐷) ≠ (𝑅𝐹))) → (𝑃 (𝑅𝑁)) = (𝑃 (𝑁𝑃)))
2015, 19eqtr2d 2834 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ (𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐷) ≠ (𝑅𝐹))) → (𝑃 (𝑁𝑃)) = (𝑃 (𝑅𝐹)))
2113, 20breqtrd 5057 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ (𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐷) ≠ (𝑅𝐹))) → (𝑁𝑃) (𝑃 (𝑅𝐹)))
22 cdlemk1.b . . 3 𝐵 = (Base‘𝐾)
23 cdlemk1.m . . 3 = (meet‘𝐾)
24 cdlemk1.s . . 3 𝑆 = (𝑓𝑇 ↦ (𝑖𝑇 (𝑖𝑃) = ((𝑃 (𝑅𝑓)) ((𝑁𝑃) (𝑅‘(𝑓𝐹))))))
25 cdlemk1.o . . 3 𝑂 = (𝑆𝐷)
2622, 5, 11, 23, 6, 7, 8, 17, 24, 25cdlemk14 38169 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ (𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐷) ≠ (𝑅𝐹))) → (𝑁𝑃) ((𝑂𝑃) (𝑅‘(𝐹𝐷))))
271hllatd 36679 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ (𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐷) ≠ (𝑅𝐹))) → 𝐾 ∈ Lat)
2822, 6atbase 36604 . . . 4 ((𝑁𝑃) ∈ 𝐴 → (𝑁𝑃) ∈ 𝐵)
2910, 28syl 17 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ (𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐷) ≠ (𝑅𝐹))) → (𝑁𝑃) ∈ 𝐵)
30 simp12 1201 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ (𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐷) ≠ (𝑅𝐹))) → 𝐹𝑇)
31 simp31 1206 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ (𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐷) ≠ (𝑅𝐹))) → 𝐹 ≠ ( I ↾ 𝐵))
3222, 6, 7, 8, 17trlnidat 37488 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵)) → (𝑅𝐹) ∈ 𝐴)
333, 30, 31, 32syl3anc 1368 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ (𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐷) ≠ (𝑅𝐹))) → (𝑅𝐹) ∈ 𝐴)
3422, 11, 6hlatjcl 36682 . . . 4 ((𝐾 ∈ HL ∧ 𝑃𝐴 ∧ (𝑅𝐹) ∈ 𝐴) → (𝑃 (𝑅𝐹)) ∈ 𝐵)
351, 2, 33, 34syl3anc 1368 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ (𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐷) ≠ (𝑅𝐹))) → (𝑃 (𝑅𝐹)) ∈ 𝐵)
3625fveq1i 6647 . . . . 5 (𝑂𝑃) = ((𝑆𝐷)‘𝑃)
3722, 5, 11, 6, 7, 8, 17, 23, 24cdlemksat 38161 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ (𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐷) ≠ (𝑅𝐹))) → ((𝑆𝐷)‘𝑃) ∈ 𝐴)
3836, 37eqeltrid 2894 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ (𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐷) ≠ (𝑅𝐹))) → (𝑂𝑃) ∈ 𝐴)
39 simp13 1202 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ (𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐷) ≠ (𝑅𝐹))) → 𝐷𝑇)
40 simp33 1208 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ (𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐷) ≠ (𝑅𝐹))) → (𝑅𝐷) ≠ (𝑅𝐹))
4140necomd 3042 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ (𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐷) ≠ (𝑅𝐹))) → (𝑅𝐹) ≠ (𝑅𝐷))
426, 7, 8, 17trlcocnvat 38039 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐷𝑇) ∧ (𝑅𝐹) ≠ (𝑅𝐷)) → (𝑅‘(𝐹𝐷)) ∈ 𝐴)
433, 30, 39, 41, 42syl121anc 1372 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ (𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐷) ≠ (𝑅𝐹))) → (𝑅‘(𝐹𝐷)) ∈ 𝐴)
4422, 11, 6hlatjcl 36682 . . . 4 ((𝐾 ∈ HL ∧ (𝑂𝑃) ∈ 𝐴 ∧ (𝑅‘(𝐹𝐷)) ∈ 𝐴) → ((𝑂𝑃) (𝑅‘(𝐹𝐷))) ∈ 𝐵)
451, 38, 43, 44syl3anc 1368 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ (𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐷) ≠ (𝑅𝐹))) → ((𝑂𝑃) (𝑅‘(𝐹𝐷))) ∈ 𝐵)
4622, 5, 23latlem12 17683 . . 3 ((𝐾 ∈ Lat ∧ ((𝑁𝑃) ∈ 𝐵 ∧ (𝑃 (𝑅𝐹)) ∈ 𝐵 ∧ ((𝑂𝑃) (𝑅‘(𝐹𝐷))) ∈ 𝐵)) → (((𝑁𝑃) (𝑃 (𝑅𝐹)) ∧ (𝑁𝑃) ((𝑂𝑃) (𝑅‘(𝐹𝐷)))) ↔ (𝑁𝑃) ((𝑃 (𝑅𝐹)) ((𝑂𝑃) (𝑅‘(𝐹𝐷))))))
4727, 29, 35, 45, 46syl13anc 1369 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ (𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐷) ≠ (𝑅𝐹))) → (((𝑁𝑃) (𝑃 (𝑅𝐹)) ∧ (𝑁𝑃) ((𝑂𝑃) (𝑅‘(𝐹𝐷)))) ↔ (𝑁𝑃) ((𝑃 (𝑅𝐹)) ((𝑂𝑃) (𝑅‘(𝐹𝐷))))))
4821, 26, 47mpbi2and 711 1 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ (𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐷) ≠ (𝑅𝐹))) → (𝑁𝑃) ((𝑃 (𝑅𝐹)) ((𝑂𝑃) (𝑅‘(𝐹𝐷)))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2987   class class class wbr 5031   ↦ cmpt 5111   I cid 5425  ◡ccnv 5519   ↾ cres 5522   ∘ ccom 5524  ‘cfv 6325  ℩crio 7093  (class class class)co 7136  Basecbs 16478  lecple 16567  joincjn 17549  meetcmee 17550  Latclat 17650  Atomscatm 36578  HLchlt 36665  LHypclh 37299  LTrncltrn 37416  trLctrl 37473 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7444  ax-riotaBAD 36268 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-iun 4884  df-iin 4885  df-br 5032  df-opab 5094  df-mpt 5112  df-id 5426  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-iota 6284  df-fun 6327  df-fn 6328  df-f 6329  df-f1 6330  df-fo 6331  df-f1o 6332  df-fv 6333  df-riota 7094  df-ov 7139  df-oprab 7140  df-mpo 7141  df-1st 7674  df-2nd 7675  df-undef 7925  df-map 8394  df-proset 17533  df-poset 17551  df-plt 17563  df-lub 17579  df-glb 17580  df-join 17581  df-meet 17582  df-p0 17644  df-p1 17645  df-lat 17651  df-clat 17713  df-oposet 36491  df-ol 36493  df-oml 36494  df-covers 36581  df-ats 36582  df-atl 36613  df-cvlat 36637  df-hlat 36666  df-llines 36813  df-lplanes 36814  df-lvols 36815  df-lines 36816  df-psubsp 36818  df-pmap 36819  df-padd 37111  df-lhyp 37303  df-laut 37304  df-ldil 37419  df-ltrn 37420  df-trl 37474 This theorem is referenced by:  cdlemk17  38173  cdlemk15-2N  38194
 Copyright terms: Public domain W3C validator