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

Theorem cdlemg46 36516
Description: Part of proof of Lemma G of [Crawley] p. 116, seventh line of third paragraph on p. 117: "hf and f have different traces." (Contributed by NM, 5-Jun-2013.)
Hypotheses
Ref Expression
cdlemg46.b 𝐵 = (Base‘𝐾)
cdlemg46.h 𝐻 = (LHyp‘𝐾)
cdlemg46.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
cdlemg46.r 𝑅 = ((trL‘𝐾)‘𝑊)
Assertion
Ref Expression
cdlemg46 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → (𝑅‘(𝐹)) ≠ (𝑅𝐹))
Distinct variable groups:   ,𝐹   ,𝐻   ,𝐾   𝑅,   𝑇,   ,𝑊
Allowed substitution hint:   𝐵()

Proof of Theorem cdlemg46
StepHypRef Expression
1 simpl1l 1286 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → 𝐾 ∈ HL)
2 simp1 1159 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
3 simp2r 1250 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → 𝑇)
4 simp32 1260 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → ≠ ( I ↾ 𝐵))
5 cdlemg46.b . . . . . 6 𝐵 = (Base‘𝐾)
6 eqid 2806 . . . . . 6 (Atoms‘𝐾) = (Atoms‘𝐾)
7 cdlemg46.h . . . . . 6 𝐻 = (LHyp‘𝐾)
8 cdlemg46.t . . . . . 6 𝑇 = ((LTrn‘𝐾)‘𝑊)
9 cdlemg46.r . . . . . 6 𝑅 = ((trL‘𝐾)‘𝑊)
105, 6, 7, 8, 9trlnidat 35954 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑇 ≠ ( I ↾ 𝐵)) → (𝑅) ∈ (Atoms‘𝐾))
112, 3, 4, 10syl3anc 1483 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → (𝑅) ∈ (Atoms‘𝐾))
1211adantr 468 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → (𝑅) ∈ (Atoms‘𝐾))
13 simp2l 1249 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → 𝐹𝑇)
14 simp31 1259 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → 𝐹 ≠ ( I ↾ 𝐵))
155, 6, 7, 8, 9trlnidat 35954 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵)) → (𝑅𝐹) ∈ (Atoms‘𝐾))
162, 13, 14, 15syl3anc 1483 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → (𝑅𝐹) ∈ (Atoms‘𝐾))
1716adantr 468 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → (𝑅𝐹) ∈ (Atoms‘𝐾))
18 simpl33 1338 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → (𝑅) ≠ (𝑅𝐹))
19 simpr 473 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → (𝑅‘(𝐹)) ∈ (Atoms‘𝐾))
207, 8ltrnco 36500 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑇𝐹𝑇) → (𝐹) ∈ 𝑇)
212, 3, 13, 20syl3anc 1483 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → (𝐹) ∈ 𝑇)
227, 8ltrncnv 35926 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) → 𝐹𝑇)
232, 13, 22syl2anc 575 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → 𝐹𝑇)
24 eqid 2806 . . . . . . . 8 (le‘𝐾) = (le‘𝐾)
25 eqid 2806 . . . . . . . 8 (join‘𝐾) = (join‘𝐾)
2624, 25, 7, 8, 9trlco 36508 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹) ∈ 𝑇𝐹𝑇) → (𝑅‘((𝐹) ∘ 𝐹))(le‘𝐾)((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹)))
272, 21, 23, 26syl3anc 1483 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → (𝑅‘((𝐹) ∘ 𝐹))(le‘𝐾)((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹)))
28 coass 5868 . . . . . . . 8 ((𝐹) ∘ 𝐹) = ( ∘ (𝐹𝐹))
295, 7, 8ltrn1o 35904 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) → 𝐹:𝐵1-1-onto𝐵)
302, 13, 29syl2anc 575 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → 𝐹:𝐵1-1-onto𝐵)
31 f1ococnv2 6379 . . . . . . . . . . 11 (𝐹:𝐵1-1-onto𝐵 → (𝐹𝐹) = ( I ↾ 𝐵))
3230, 31syl 17 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → (𝐹𝐹) = ( I ↾ 𝐵))
3332coeq2d 5486 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → ( ∘ (𝐹𝐹)) = ( ∘ ( I ↾ 𝐵)))
345, 7, 8ltrn1o 35904 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑇) → :𝐵1-1-onto𝐵)
352, 3, 34syl2anc 575 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → :𝐵1-1-onto𝐵)
36 f1of 6353 . . . . . . . . . 10 (:𝐵1-1-onto𝐵:𝐵𝐵)
37 fcoi1 6293 . . . . . . . . . 10 (:𝐵𝐵 → ( ∘ ( I ↾ 𝐵)) = )
3835, 36, 373syl 18 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → ( ∘ ( I ↾ 𝐵)) = )
3933, 38eqtrd 2840 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → ( ∘ (𝐹𝐹)) = )
4028, 39syl5eq 2852 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → ((𝐹) ∘ 𝐹) = )
4140fveq2d 6412 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → (𝑅‘((𝐹) ∘ 𝐹)) = (𝑅))
427, 8, 9trlcnv 35946 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) → (𝑅𝐹) = (𝑅𝐹))
432, 13, 42syl2anc 575 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → (𝑅𝐹) = (𝑅𝐹))
4443oveq2d 6890 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → ((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹)) = ((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹)))
4527, 41, 443brtr3d 4875 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → (𝑅)(le‘𝐾)((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹)))
4645adantr 468 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → (𝑅)(le‘𝐾)((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹)))
4724, 25, 6hlatlej2 35156 . . . . 5 ((𝐾 ∈ HL ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾) ∧ (𝑅𝐹) ∈ (Atoms‘𝐾)) → (𝑅𝐹)(le‘𝐾)((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹)))
481, 19, 17, 47syl3anc 1483 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → (𝑅𝐹)(le‘𝐾)((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹)))
491hllatd 35144 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → 𝐾 ∈ Lat)
505, 6atbase 35069 . . . . . 6 ((𝑅) ∈ (Atoms‘𝐾) → (𝑅) ∈ 𝐵)
5112, 50syl 17 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → (𝑅) ∈ 𝐵)
525, 6atbase 35069 . . . . . 6 ((𝑅𝐹) ∈ (Atoms‘𝐾) → (𝑅𝐹) ∈ 𝐵)
5317, 52syl 17 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → (𝑅𝐹) ∈ 𝐵)
545, 25, 6hlatjcl 35147 . . . . . 6 ((𝐾 ∈ HL ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾) ∧ (𝑅𝐹) ∈ (Atoms‘𝐾)) → ((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹)) ∈ 𝐵)
551, 19, 17, 54syl3anc 1483 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → ((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹)) ∈ 𝐵)
565, 24, 25latjle12 17267 . . . . 5 ((𝐾 ∈ Lat ∧ ((𝑅) ∈ 𝐵 ∧ (𝑅𝐹) ∈ 𝐵 ∧ ((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹)) ∈ 𝐵)) → (((𝑅)(le‘𝐾)((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹)) ∧ (𝑅𝐹)(le‘𝐾)((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹))) ↔ ((𝑅)(join‘𝐾)(𝑅𝐹))(le‘𝐾)((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹))))
5749, 51, 53, 55, 56syl13anc 1484 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → (((𝑅)(le‘𝐾)((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹)) ∧ (𝑅𝐹)(le‘𝐾)((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹))) ↔ ((𝑅)(join‘𝐾)(𝑅𝐹))(le‘𝐾)((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹))))
5846, 48, 57mpbi2and 694 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → ((𝑅)(join‘𝐾)(𝑅𝐹))(le‘𝐾)((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹)))
5924, 25, 62atjlej 35259 . . 3 ((𝐾 ∈ HL ∧ ((𝑅) ∈ (Atoms‘𝐾) ∧ (𝑅𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅) ≠ (𝑅𝐹)) ∧ ((𝑅‘(𝐹)) ∈ (Atoms‘𝐾) ∧ (𝑅𝐹) ∈ (Atoms‘𝐾) ∧ ((𝑅)(join‘𝐾)(𝑅𝐹))(le‘𝐾)((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹)))) → (𝑅‘(𝐹)) ≠ (𝑅𝐹))
601, 12, 17, 18, 19, 17, 58, 59syl133anc 1505 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → (𝑅‘(𝐹)) ≠ (𝑅𝐹))
61 nelne2 3075 . . . 4 (((𝑅𝐹) ∈ (Atoms‘𝐾) ∧ ¬ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → (𝑅𝐹) ≠ (𝑅‘(𝐹)))
6261necomd 3033 . . 3 (((𝑅𝐹) ∈ (Atoms‘𝐾) ∧ ¬ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → (𝑅‘(𝐹)) ≠ (𝑅𝐹))
6316, 62sylan 571 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) ∧ ¬ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → (𝑅‘(𝐹)) ≠ (𝑅𝐹))
6460, 63pm2.61dan 838 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → (𝑅‘(𝐹)) ≠ (𝑅𝐹))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wcel 2156  wne 2978   class class class wbr 4844   I cid 5218  ccnv 5310  cres 5313  ccom 5315  wf 6097  1-1-ontowf1o 6100  cfv 6101  (class class class)co 6874  Basecbs 16068  lecple 16160  joincjn 17149  Latclat 17250  Atomscatm 35043  HLchlt 35130  LHypclh 35764  LTrncltrn 35881  trLctrl 35939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179  ax-riotaBAD 34732
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-iun 4714  df-iin 4715  df-br 4845  df-opab 4907  df-mpt 4924  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-riota 6835  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-1st 7398  df-2nd 7399  df-undef 7634  df-map 8094  df-proset 17133  df-poset 17151  df-plt 17163  df-lub 17179  df-glb 17180  df-join 17181  df-meet 17182  df-p0 17244  df-p1 17245  df-lat 17251  df-clat 17313  df-oposet 34956  df-ol 34958  df-oml 34959  df-covers 35046  df-ats 35047  df-atl 35078  df-cvlat 35102  df-hlat 35131  df-llines 35278  df-lplanes 35279  df-lvols 35280  df-lines 35281  df-psubsp 35283  df-pmap 35284  df-padd 35576  df-lhyp 35768  df-laut 35769  df-ldil 35884  df-ltrn 35885  df-trl 35940
This theorem is referenced by:  cdlemg47  36517
  Copyright terms: Public domain W3C validator