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

Theorem cvlcvr1 35113
Description: The covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 29536 analog.) (Contributed by NM, 5-Nov-2012.)
Hypotheses
Ref Expression
cvlcvr1.b 𝐵 = (Base‘𝐾)
cvlcvr1.l = (le‘𝐾)
cvlcvr1.j = (join‘𝐾)
cvlcvr1.c 𝐶 = ( ⋖ ‘𝐾)
cvlcvr1.a 𝐴 = (Atoms‘𝐾)
Assertion
Ref Expression
cvlcvr1 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → (¬ 𝑃 𝑋𝑋𝐶(𝑋 𝑃)))

Proof of Theorem cvlcvr1
Dummy variables 𝑧 𝑞 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp13 1255 . . . . . . 7 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → 𝐾 ∈ CvLat)
2 cvllat 35100 . . . . . . 7 (𝐾 ∈ CvLat → 𝐾 ∈ Lat)
31, 2syl 17 . . . . . 6 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → 𝐾 ∈ Lat)
4 simp2 1160 . . . . . 6 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → 𝑋𝐵)
5 cvlcvr1.b . . . . . . . 8 𝐵 = (Base‘𝐾)
6 cvlcvr1.a . . . . . . . 8 𝐴 = (Atoms‘𝐾)
75, 6atbase 35063 . . . . . . 7 (𝑃𝐴𝑃𝐵)
873ad2ant3 1158 . . . . . 6 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → 𝑃𝐵)
9 cvlcvr1.l . . . . . . 7 = (le‘𝐾)
10 eqid 2802 . . . . . . 7 (lt‘𝐾) = (lt‘𝐾)
11 cvlcvr1.j . . . . . . 7 = (join‘𝐾)
125, 9, 10, 11latnle 17284 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑃𝐵) → (¬ 𝑃 𝑋𝑋(lt‘𝐾)(𝑋 𝑃)))
133, 4, 8, 12syl3anc 1483 . . . . 5 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → (¬ 𝑃 𝑋𝑋(lt‘𝐾)(𝑋 𝑃)))
1413biimpd 220 . . . 4 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → (¬ 𝑃 𝑋𝑋(lt‘𝐾)(𝑋 𝑃)))
15 simpl13 1326 . . . . . . . . 9 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → 𝐾 ∈ CvLat)
1615, 2syl 17 . . . . . . . 8 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → 𝐾 ∈ Lat)
17 simprll 788 . . . . . . . 8 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → 𝑧𝐵)
18 simpl2 1237 . . . . . . . . 9 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → 𝑋𝐵)
19 simpl3 1239 . . . . . . . . . 10 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → 𝑃𝐴)
2019, 7syl 17 . . . . . . . . 9 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → 𝑃𝐵)
215, 11latjcl 17250 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑃𝐵) → (𝑋 𝑃) ∈ 𝐵)
2216, 18, 20, 21syl3anc 1483 . . . . . . . 8 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → (𝑋 𝑃) ∈ 𝐵)
23 simprrr 791 . . . . . . . 8 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → 𝑧 (𝑋 𝑃))
24 simprrl 790 . . . . . . . . . 10 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → 𝑋(lt‘𝐾)𝑧)
25 simpl11 1322 . . . . . . . . . . 11 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → 𝐾 ∈ OML)
26 simpl12 1324 . . . . . . . . . . 11 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → 𝐾 ∈ CLat)
27 cvlatl 35099 . . . . . . . . . . . 12 (𝐾 ∈ CvLat → 𝐾 ∈ AtLat)
2815, 27syl 17 . . . . . . . . . . 11 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → 𝐾 ∈ AtLat)
295, 9, 10, 6atlrelat1 35095 . . . . . . . . . . 11 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵𝑧𝐵) → (𝑋(lt‘𝐾)𝑧 → ∃𝑞𝐴𝑞 𝑋𝑞 𝑧)))
3025, 26, 28, 18, 17, 29syl311anc 1496 . . . . . . . . . 10 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → (𝑋(lt‘𝐾)𝑧 → ∃𝑞𝐴𝑞 𝑋𝑞 𝑧)))
3124, 30mpd 15 . . . . . . . . 9 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → ∃𝑞𝐴𝑞 𝑋𝑞 𝑧))
3216adantr 468 . . . . . . . . . . . . 13 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → 𝐾 ∈ Lat)
335, 6atbase 35063 . . . . . . . . . . . . . 14 (𝑞𝐴𝑞𝐵)
3433ad2antrl 710 . . . . . . . . . . . . 13 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → 𝑞𝐵)
3517adantr 468 . . . . . . . . . . . . 13 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → 𝑧𝐵)
3622adantr 468 . . . . . . . . . . . . 13 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → (𝑋 𝑃) ∈ 𝐵)
37 simprrr 791 . . . . . . . . . . . . 13 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → 𝑞 𝑧)
3823adantr 468 . . . . . . . . . . . . 13 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → 𝑧 (𝑋 𝑃))
395, 9, 32, 34, 35, 36, 37, 38lattrd 17257 . . . . . . . . . . . 12 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → 𝑞 (𝑋 𝑃))
4015adantr 468 . . . . . . . . . . . . 13 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → 𝐾 ∈ CvLat)
41 simprl 778 . . . . . . . . . . . . 13 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → 𝑞𝐴)
42 simpll3 1266 . . . . . . . . . . . . 13 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → 𝑃𝐴)
43 simpll2 1264 . . . . . . . . . . . . 13 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → 𝑋𝐵)
44 simprrl 790 . . . . . . . . . . . . 13 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → ¬ 𝑞 𝑋)
455, 9, 11, 6cvlexch1 35102 . . . . . . . . . . . . 13 ((𝐾 ∈ CvLat ∧ (𝑞𝐴𝑃𝐴𝑋𝐵) ∧ ¬ 𝑞 𝑋) → (𝑞 (𝑋 𝑃) → 𝑃 (𝑋 𝑞)))
4640, 41, 42, 43, 44, 45syl131anc 1495 . . . . . . . . . . . 12 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → (𝑞 (𝑋 𝑃) → 𝑃 (𝑋 𝑞)))
4739, 46mpd 15 . . . . . . . . . . 11 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → 𝑃 (𝑋 𝑞))
48 simprlr 789 . . . . . . . . . . . . 13 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → ¬ 𝑃 𝑋)
4948adantr 468 . . . . . . . . . . . 12 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → ¬ 𝑃 𝑋)
505, 9, 11, 6cvlexchb1 35104 . . . . . . . . . . . 12 ((𝐾 ∈ CvLat ∧ (𝑃𝐴𝑞𝐴𝑋𝐵) ∧ ¬ 𝑃 𝑋) → (𝑃 (𝑋 𝑞) ↔ (𝑋 𝑃) = (𝑋 𝑞)))
5140, 42, 41, 43, 49, 50syl131anc 1495 . . . . . . . . . . 11 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → (𝑃 (𝑋 𝑞) ↔ (𝑋 𝑃) = (𝑋 𝑞)))
5247, 51mpbid 223 . . . . . . . . . 10 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → (𝑋 𝑃) = (𝑋 𝑞))
539, 10pltle 17160 . . . . . . . . . . . . . 14 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑧𝐵) → (𝑋(lt‘𝐾)𝑧𝑋 𝑧))
5425, 18, 17, 53syl3anc 1483 . . . . . . . . . . . . 13 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → (𝑋(lt‘𝐾)𝑧𝑋 𝑧))
5524, 54mpd 15 . . . . . . . . . . . 12 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → 𝑋 𝑧)
5655adantr 468 . . . . . . . . . . 11 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → 𝑋 𝑧)
575, 9, 11latjle12 17261 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (𝑋𝐵𝑞𝐵𝑧𝐵)) → ((𝑋 𝑧𝑞 𝑧) ↔ (𝑋 𝑞) 𝑧))
5832, 43, 34, 35, 57syl13anc 1484 . . . . . . . . . . 11 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → ((𝑋 𝑧𝑞 𝑧) ↔ (𝑋 𝑞) 𝑧))
5956, 37, 58mpbi2and 694 . . . . . . . . . 10 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → (𝑋 𝑞) 𝑧)
6052, 59eqbrtrd 4859 . . . . . . . . 9 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → (𝑋 𝑃) 𝑧)
6131, 60rexlimddv 3219 . . . . . . . 8 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → (𝑋 𝑃) 𝑧)
625, 9, 16, 17, 22, 23, 61latasymd 17256 . . . . . . 7 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → 𝑧 = (𝑋 𝑃))
6362exp44 426 . . . . . 6 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → (𝑧𝐵 → (¬ 𝑃 𝑋 → ((𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)) → 𝑧 = (𝑋 𝑃)))))
6463imp 395 . . . . 5 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑧𝐵) → (¬ 𝑃 𝑋 → ((𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)) → 𝑧 = (𝑋 𝑃))))
6564ralrimdva 3153 . . . 4 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → (¬ 𝑃 𝑋 → ∀𝑧𝐵 ((𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)) → 𝑧 = (𝑋 𝑃))))
6614, 65jcad 504 . . 3 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → (¬ 𝑃 𝑋 → (𝑋(lt‘𝐾)(𝑋 𝑃) ∧ ∀𝑧𝐵 ((𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)) → 𝑧 = (𝑋 𝑃)))))
673, 4, 8, 21syl3anc 1483 . . . 4 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → (𝑋 𝑃) ∈ 𝐵)
68 cvlcvr1.c . . . . 5 𝐶 = ( ⋖ ‘𝐾)
695, 9, 10, 68cvrval2 35048 . . . 4 ((𝐾 ∈ Lat ∧ 𝑋𝐵 ∧ (𝑋 𝑃) ∈ 𝐵) → (𝑋𝐶(𝑋 𝑃) ↔ (𝑋(lt‘𝐾)(𝑋 𝑃) ∧ ∀𝑧𝐵 ((𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)) → 𝑧 = (𝑋 𝑃)))))
703, 4, 67, 69syl3anc 1483 . . 3 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → (𝑋𝐶(𝑋 𝑃) ↔ (𝑋(lt‘𝐾)(𝑋 𝑃) ∧ ∀𝑧𝐵 ((𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)) → 𝑧 = (𝑋 𝑃)))))
7166, 70sylibrd 250 . 2 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → (¬ 𝑃 𝑋𝑋𝐶(𝑋 𝑃)))
723adantr 468 . . . . 5 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑋𝐶(𝑋 𝑃)) → 𝐾 ∈ Lat)
73 simpl2 1237 . . . . 5 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑋𝐶(𝑋 𝑃)) → 𝑋𝐵)
7467adantr 468 . . . . 5 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑋𝐶(𝑋 𝑃)) → (𝑋 𝑃) ∈ 𝐵)
75 simpr 473 . . . . 5 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑋𝐶(𝑋 𝑃)) → 𝑋𝐶(𝑋 𝑃))
765, 10, 68cvrlt 35044 . . . . 5 (((𝐾 ∈ Lat ∧ 𝑋𝐵 ∧ (𝑋 𝑃) ∈ 𝐵) ∧ 𝑋𝐶(𝑋 𝑃)) → 𝑋(lt‘𝐾)(𝑋 𝑃))
7772, 73, 74, 75, 76syl31anc 1485 . . . 4 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑋𝐶(𝑋 𝑃)) → 𝑋(lt‘𝐾)(𝑋 𝑃))
7877ex 399 . . 3 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → (𝑋𝐶(𝑋 𝑃) → 𝑋(lt‘𝐾)(𝑋 𝑃)))
7978, 13sylibrd 250 . 2 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → (𝑋𝐶(𝑋 𝑃) → ¬ 𝑃 𝑋))
8071, 79impbid 203 1 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → (¬ 𝑃 𝑋𝑋𝐶(𝑋 𝑃)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wcel 2155  wral 3092  wrex 3093   class class class wbr 4837  cfv 6095  (class class class)co 6868  Basecbs 16062  lecple 16154  ltcplt 17140  joincjn 17143  Latclat 17244  CLatccla 17306  OMLcoml 34949  ccvr 35036  Atomscatm 35037  AtLatcal 35038  CvLatclc 35039
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 2067  ax-7 2103  ax-8 2157  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-rep 4957  ax-sep 4968  ax-nul 4977  ax-pow 5029  ax-pr 5090  ax-un 7173
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-eu 2633  df-mo 2634  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ne 2975  df-ral 3097  df-rex 3098  df-reu 3099  df-rab 3101  df-v 3389  df-sbc 3628  df-csb 3723  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-nul 4111  df-if 4274  df-pw 4347  df-sn 4365  df-pr 4367  df-op 4371  df-uni 4624  df-iun 4707  df-br 4838  df-opab 4900  df-mpt 4917  df-id 5213  df-xp 5311  df-rel 5312  df-cnv 5313  df-co 5314  df-dm 5315  df-rn 5316  df-res 5317  df-ima 5318  df-iota 6058  df-fun 6097  df-fn 6098  df-f 6099  df-f1 6100  df-fo 6101  df-f1o 6102  df-fv 6103  df-riota 6829  df-ov 6871  df-oprab 6872  df-proset 17127  df-poset 17145  df-plt 17157  df-lub 17173  df-glb 17174  df-join 17175  df-meet 17176  df-p0 17238  df-lat 17245  df-clat 17307  df-oposet 34950  df-ol 34952  df-oml 34953  df-covers 35040  df-ats 35041  df-atl 35072  df-cvlat 35096
This theorem is referenced by:  cvlcvrp  35114  cvr1  35184
  Copyright terms: Public domain W3C validator