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

Theorem cvlcvr1 36628
 Description: The covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 30141 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 1202 . . . . . . 7 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → 𝐾 ∈ CvLat)
2 cvllat 36615 . . . . . . 7 (𝐾 ∈ CvLat → 𝐾 ∈ Lat)
31, 2syl 17 . . . . . 6 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → 𝐾 ∈ Lat)
4 simp2 1134 . . . . . 6 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → 𝑋𝐵)
5 cvlcvr1.b . . . . . . . 8 𝐵 = (Base‘𝐾)
6 cvlcvr1.a . . . . . . . 8 𝐴 = (Atoms‘𝐾)
75, 6atbase 36578 . . . . . . 7 (𝑃𝐴𝑃𝐵)
873ad2ant3 1132 . . . . . 6 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → 𝑃𝐵)
9 cvlcvr1.l . . . . . . 7 = (le‘𝐾)
10 eqid 2801 . . . . . . 7 (lt‘𝐾) = (lt‘𝐾)
11 cvlcvr1.j . . . . . . 7 = (join‘𝐾)
125, 9, 10, 11latnle 17690 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑃𝐵) → (¬ 𝑃 𝑋𝑋(lt‘𝐾)(𝑋 𝑃)))
133, 4, 8, 12syl3anc 1368 . . . . 5 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → (¬ 𝑃 𝑋𝑋(lt‘𝐾)(𝑋 𝑃)))
1413biimpd 232 . . . 4 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → (¬ 𝑃 𝑋𝑋(lt‘𝐾)(𝑋 𝑃)))
15 simpl13 1247 . . . . . . . . 9 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → 𝐾 ∈ CvLat)
1615, 2syl 17 . . . . . . . 8 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → 𝐾 ∈ Lat)
17 simprll 778 . . . . . . . 8 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → 𝑧𝐵)
18 simpl2 1189 . . . . . . . . 9 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → 𝑋𝐵)
19 simpl3 1190 . . . . . . . . . 10 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → 𝑃𝐴)
2019, 7syl 17 . . . . . . . . 9 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → 𝑃𝐵)
215, 11latjcl 17656 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑃𝐵) → (𝑋 𝑃) ∈ 𝐵)
2216, 18, 20, 21syl3anc 1368 . . . . . . . 8 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → (𝑋 𝑃) ∈ 𝐵)
23 simprrr 781 . . . . . . . 8 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → 𝑧 (𝑋 𝑃))
24 simprrl 780 . . . . . . . . . 10 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → 𝑋(lt‘𝐾)𝑧)
25 simpl11 1245 . . . . . . . . . . 11 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → 𝐾 ∈ OML)
26 simpl12 1246 . . . . . . . . . . 11 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → 𝐾 ∈ CLat)
27 cvlatl 36614 . . . . . . . . . . . 12 (𝐾 ∈ CvLat → 𝐾 ∈ AtLat)
2815, 27syl 17 . . . . . . . . . . 11 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → 𝐾 ∈ AtLat)
295, 9, 10, 6atlrelat1 36610 . . . . . . . . . . 11 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵𝑧𝐵) → (𝑋(lt‘𝐾)𝑧 → ∃𝑞𝐴𝑞 𝑋𝑞 𝑧)))
3025, 26, 28, 18, 17, 29syl311anc 1381 . . . . . . . . . 10 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → (𝑋(lt‘𝐾)𝑧 → ∃𝑞𝐴𝑞 𝑋𝑞 𝑧)))
3124, 30mpd 15 . . . . . . . . 9 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → ∃𝑞𝐴𝑞 𝑋𝑞 𝑧))
3216adantr 484 . . . . . . . . . . . . 13 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → 𝐾 ∈ Lat)
335, 6atbase 36578 . . . . . . . . . . . . . 14 (𝑞𝐴𝑞𝐵)
3433ad2antrl 727 . . . . . . . . . . . . 13 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → 𝑞𝐵)
3517adantr 484 . . . . . . . . . . . . 13 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → 𝑧𝐵)
3622adantr 484 . . . . . . . . . . . . 13 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → (𝑋 𝑃) ∈ 𝐵)
37 simprrr 781 . . . . . . . . . . . . 13 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → 𝑞 𝑧)
3823adantr 484 . . . . . . . . . . . . 13 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → 𝑧 (𝑋 𝑃))
395, 9, 32, 34, 35, 36, 37, 38lattrd 17663 . . . . . . . . . . . 12 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → 𝑞 (𝑋 𝑃))
4015adantr 484 . . . . . . . . . . . . 13 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → 𝐾 ∈ CvLat)
41 simprl 770 . . . . . . . . . . . . 13 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → 𝑞𝐴)
42 simpll3 1211 . . . . . . . . . . . . 13 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → 𝑃𝐴)
43 simpll2 1210 . . . . . . . . . . . . 13 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → 𝑋𝐵)
44 simprrl 780 . . . . . . . . . . . . 13 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → ¬ 𝑞 𝑋)
455, 9, 11, 6cvlexch1 36617 . . . . . . . . . . . . 13 ((𝐾 ∈ CvLat ∧ (𝑞𝐴𝑃𝐴𝑋𝐵) ∧ ¬ 𝑞 𝑋) → (𝑞 (𝑋 𝑃) → 𝑃 (𝑋 𝑞)))
4640, 41, 42, 43, 44, 45syl131anc 1380 . . . . . . . . . . . 12 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → (𝑞 (𝑋 𝑃) → 𝑃 (𝑋 𝑞)))
4739, 46mpd 15 . . . . . . . . . . 11 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → 𝑃 (𝑋 𝑞))
48 simprlr 779 . . . . . . . . . . . . 13 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → ¬ 𝑃 𝑋)
4948adantr 484 . . . . . . . . . . . 12 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → ¬ 𝑃 𝑋)
505, 9, 11, 6cvlexchb1 36619 . . . . . . . . . . . 12 ((𝐾 ∈ CvLat ∧ (𝑃𝐴𝑞𝐴𝑋𝐵) ∧ ¬ 𝑃 𝑋) → (𝑃 (𝑋 𝑞) ↔ (𝑋 𝑃) = (𝑋 𝑞)))
5140, 42, 41, 43, 49, 50syl131anc 1380 . . . . . . . . . . 11 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → (𝑃 (𝑋 𝑞) ↔ (𝑋 𝑃) = (𝑋 𝑞)))
5247, 51mpbid 235 . . . . . . . . . 10 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → (𝑋 𝑃) = (𝑋 𝑞))
539, 10pltle 17566 . . . . . . . . . . . . . 14 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑧𝐵) → (𝑋(lt‘𝐾)𝑧𝑋 𝑧))
5425, 18, 17, 53syl3anc 1368 . . . . . . . . . . . . 13 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → (𝑋(lt‘𝐾)𝑧𝑋 𝑧))
5524, 54mpd 15 . . . . . . . . . . . 12 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → 𝑋 𝑧)
5655adantr 484 . . . . . . . . . . 11 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → 𝑋 𝑧)
575, 9, 11latjle12 17667 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (𝑋𝐵𝑞𝐵𝑧𝐵)) → ((𝑋 𝑧𝑞 𝑧) ↔ (𝑋 𝑞) 𝑧))
5832, 43, 34, 35, 57syl13anc 1369 . . . . . . . . . . 11 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → ((𝑋 𝑧𝑞 𝑧) ↔ (𝑋 𝑞) 𝑧))
5956, 37, 58mpbi2and 711 . . . . . . . . . 10 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → (𝑋 𝑞) 𝑧)
6052, 59eqbrtrd 5055 . . . . . . . . 9 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑋𝑞 𝑧))) → (𝑋 𝑃) 𝑧)
6131, 60rexlimddv 3253 . . . . . . . 8 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → (𝑋 𝑃) 𝑧)
625, 9, 16, 17, 22, 23, 61latasymd 17662 . . . . . . 7 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ ((𝑧𝐵 ∧ ¬ 𝑃 𝑋) ∧ (𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)))) → 𝑧 = (𝑋 𝑃))
6362exp44 441 . . . . . 6 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → (𝑧𝐵 → (¬ 𝑃 𝑋 → ((𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)) → 𝑧 = (𝑋 𝑃)))))
6463imp 410 . . . . 5 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑧𝐵) → (¬ 𝑃 𝑋 → ((𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)) → 𝑧 = (𝑋 𝑃))))
6564ralrimdva 3157 . . . 4 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → (¬ 𝑃 𝑋 → ∀𝑧𝐵 ((𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)) → 𝑧 = (𝑋 𝑃))))
6614, 65jcad 516 . . 3 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → (¬ 𝑃 𝑋 → (𝑋(lt‘𝐾)(𝑋 𝑃) ∧ ∀𝑧𝐵 ((𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)) → 𝑧 = (𝑋 𝑃)))))
673, 4, 8, 21syl3anc 1368 . . . 4 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → (𝑋 𝑃) ∈ 𝐵)
68 cvlcvr1.c . . . . 5 𝐶 = ( ⋖ ‘𝐾)
695, 9, 10, 68cvrval2 36563 . . . 4 ((𝐾 ∈ Lat ∧ 𝑋𝐵 ∧ (𝑋 𝑃) ∈ 𝐵) → (𝑋𝐶(𝑋 𝑃) ↔ (𝑋(lt‘𝐾)(𝑋 𝑃) ∧ ∀𝑧𝐵 ((𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)) → 𝑧 = (𝑋 𝑃)))))
703, 4, 67, 69syl3anc 1368 . . 3 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → (𝑋𝐶(𝑋 𝑃) ↔ (𝑋(lt‘𝐾)(𝑋 𝑃) ∧ ∀𝑧𝐵 ((𝑋(lt‘𝐾)𝑧𝑧 (𝑋 𝑃)) → 𝑧 = (𝑋 𝑃)))))
7166, 70sylibrd 262 . 2 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → (¬ 𝑃 𝑋𝑋𝐶(𝑋 𝑃)))
723adantr 484 . . . . 5 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑋𝐶(𝑋 𝑃)) → 𝐾 ∈ Lat)
73 simpl2 1189 . . . . 5 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑋𝐶(𝑋 𝑃)) → 𝑋𝐵)
7467adantr 484 . . . . 5 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑋𝐶(𝑋 𝑃)) → (𝑋 𝑃) ∈ 𝐵)
75 simpr 488 . . . . 5 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑋𝐶(𝑋 𝑃)) → 𝑋𝐶(𝑋 𝑃))
765, 10, 68cvrlt 36559 . . . . 5 (((𝐾 ∈ Lat ∧ 𝑋𝐵 ∧ (𝑋 𝑃) ∈ 𝐵) ∧ 𝑋𝐶(𝑋 𝑃)) → 𝑋(lt‘𝐾)(𝑋 𝑃))
7772, 73, 74, 75, 76syl31anc 1370 . . . 4 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑋𝐶(𝑋 𝑃)) → 𝑋(lt‘𝐾)(𝑋 𝑃))
7877ex 416 . . 3 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → (𝑋𝐶(𝑋 𝑃) → 𝑋(lt‘𝐾)(𝑋 𝑃)))
7978, 13sylibrd 262 . 2 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → (𝑋𝐶(𝑋 𝑃) → ¬ 𝑃 𝑋))
8071, 79impbid 215 1 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋𝐵𝑃𝐴) → (¬ 𝑃 𝑋𝑋𝐶(𝑋 𝑃)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2112  ∀wral 3109  ∃wrex 3110   class class class wbr 5033  ‘cfv 6328  (class class class)co 7139  Basecbs 16478  lecple 16567  ltcplt 17546  joincjn 17549  Latclat 17650  CLatccla 17712  OMLcoml 36464   ⋖ ccvr 36551  Atomscatm 36552  AtLatcal 36553  CvLatclc 36554 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 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7097  df-ov 7142  df-oprab 7143  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-lat 17651  df-clat 17713  df-oposet 36465  df-ol 36467  df-oml 36468  df-covers 36555  df-ats 36556  df-atl 36587  df-cvlat 36611 This theorem is referenced by:  cvlcvrp  36629  cvr1  36699
 Copyright terms: Public domain W3C validator