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

Theorem 2atlt 34244
 Description: Given an atom less than an element, there is another atom less than the element. (Contributed by NM, 6-May-2012.)
Hypotheses
Ref Expression
2atomslt.b 𝐵 = (Base‘𝐾)
2atomslt.s < = (lt‘𝐾)
2atomslt.a 𝐴 = (Atoms‘𝐾)
Assertion
Ref Expression
2atlt (((𝐾 ∈ HL ∧ 𝑃𝐴𝑋𝐵) ∧ 𝑃 < 𝑋) → ∃𝑞𝐴 (𝑞𝑃𝑞 < 𝑋))
Distinct variable groups:   𝐴,𝑞   𝐵,𝑞   𝐾,𝑞   𝑃,𝑞   < ,𝑞   𝑋,𝑞

Proof of Theorem 2atlt
StepHypRef Expression
1 2atomslt.b . . . 4 𝐵 = (Base‘𝐾)
2 2atomslt.a . . . 4 𝐴 = (Atoms‘𝐾)
31, 2atbase 34095 . . 3 (𝑃𝐴𝑃𝐵)
4 eqid 2621 . . . 4 (le‘𝐾) = (le‘𝐾)
5 2atomslt.s . . . 4 < = (lt‘𝐾)
6 eqid 2621 . . . 4 (join‘𝐾) = (join‘𝐾)
71, 4, 5, 6, 2hlrelat 34207 . . 3 (((𝐾 ∈ HL ∧ 𝑃𝐵𝑋𝐵) ∧ 𝑃 < 𝑋) → ∃𝑞𝐴 (𝑃 < (𝑃(join‘𝐾)𝑞) ∧ (𝑃(join‘𝐾)𝑞)(le‘𝐾)𝑋))
83, 7syl3anl2 1372 . 2 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑋𝐵) ∧ 𝑃 < 𝑋) → ∃𝑞𝐴 (𝑃 < (𝑃(join‘𝐾)𝑞) ∧ (𝑃(join‘𝐾)𝑞)(le‘𝐾)𝑋))
9 simp3l 1087 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑋𝐵) ∧ 𝑃 < 𝑋) ∧ 𝑞𝐴 ∧ (𝑃 < (𝑃(join‘𝐾)𝑞) ∧ (𝑃(join‘𝐾)𝑞)(le‘𝐾)𝑋)) → 𝑃 < (𝑃(join‘𝐾)𝑞))
10 simp1l1 1152 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑋𝐵) ∧ 𝑃 < 𝑋) ∧ 𝑞𝐴 ∧ (𝑃 < (𝑃(join‘𝐾)𝑞) ∧ (𝑃(join‘𝐾)𝑞)(le‘𝐾)𝑋)) → 𝐾 ∈ HL)
11 simp1l2 1153 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑋𝐵) ∧ 𝑃 < 𝑋) ∧ 𝑞𝐴 ∧ (𝑃 < (𝑃(join‘𝐾)𝑞) ∧ (𝑃(join‘𝐾)𝑞)(le‘𝐾)𝑋)) → 𝑃𝐴)
12 simp2 1060 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑋𝐵) ∧ 𝑃 < 𝑋) ∧ 𝑞𝐴 ∧ (𝑃 < (𝑃(join‘𝐾)𝑞) ∧ (𝑃(join‘𝐾)𝑞)(le‘𝐾)𝑋)) → 𝑞𝐴)
13 eqid 2621 . . . . . . . . . 10 ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
145, 6, 2, 13atltcvr 34240 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑃𝐴𝑞𝐴)) → (𝑃 < (𝑃(join‘𝐾)𝑞) ↔ 𝑃( ⋖ ‘𝐾)(𝑃(join‘𝐾)𝑞)))
1510, 11, 11, 12, 14syl13anc 1325 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑋𝐵) ∧ 𝑃 < 𝑋) ∧ 𝑞𝐴 ∧ (𝑃 < (𝑃(join‘𝐾)𝑞) ∧ (𝑃(join‘𝐾)𝑞)(le‘𝐾)𝑋)) → (𝑃 < (𝑃(join‘𝐾)𝑞) ↔ 𝑃( ⋖ ‘𝐾)(𝑃(join‘𝐾)𝑞)))
169, 15mpbid 222 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑋𝐵) ∧ 𝑃 < 𝑋) ∧ 𝑞𝐴 ∧ (𝑃 < (𝑃(join‘𝐾)𝑞) ∧ (𝑃(join‘𝐾)𝑞)(le‘𝐾)𝑋)) → 𝑃( ⋖ ‘𝐾)(𝑃(join‘𝐾)𝑞))
176, 13, 2atcvr1 34222 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑞𝐴) → (𝑃𝑞𝑃( ⋖ ‘𝐾)(𝑃(join‘𝐾)𝑞)))
1810, 11, 12, 17syl3anc 1323 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑋𝐵) ∧ 𝑃 < 𝑋) ∧ 𝑞𝐴 ∧ (𝑃 < (𝑃(join‘𝐾)𝑞) ∧ (𝑃(join‘𝐾)𝑞)(le‘𝐾)𝑋)) → (𝑃𝑞𝑃( ⋖ ‘𝐾)(𝑃(join‘𝐾)𝑞)))
1916, 18mpbird 247 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑋𝐵) ∧ 𝑃 < 𝑋) ∧ 𝑞𝐴 ∧ (𝑃 < (𝑃(join‘𝐾)𝑞) ∧ (𝑃(join‘𝐾)𝑞)(le‘𝐾)𝑋)) → 𝑃𝑞)
2019necomd 2845 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑋𝐵) ∧ 𝑃 < 𝑋) ∧ 𝑞𝐴 ∧ (𝑃 < (𝑃(join‘𝐾)𝑞) ∧ (𝑃(join‘𝐾)𝑞)(le‘𝐾)𝑋)) → 𝑞𝑃)
215, 6, 2atlt 34242 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑞𝐴𝑃𝐴) → (𝑞 < (𝑞(join‘𝐾)𝑃) ↔ 𝑞𝑃))
2210, 12, 11, 21syl3anc 1323 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑋𝐵) ∧ 𝑃 < 𝑋) ∧ 𝑞𝐴 ∧ (𝑃 < (𝑃(join‘𝐾)𝑞) ∧ (𝑃(join‘𝐾)𝑞)(le‘𝐾)𝑋)) → (𝑞 < (𝑞(join‘𝐾)𝑃) ↔ 𝑞𝑃))
2320, 22mpbird 247 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑋𝐵) ∧ 𝑃 < 𝑋) ∧ 𝑞𝐴 ∧ (𝑃 < (𝑃(join‘𝐾)𝑞) ∧ (𝑃(join‘𝐾)𝑞)(le‘𝐾)𝑋)) → 𝑞 < (𝑞(join‘𝐾)𝑃))
24 hllat 34169 . . . . . . . . 9 (𝐾 ∈ HL → 𝐾 ∈ Lat)
2510, 24syl 17 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑋𝐵) ∧ 𝑃 < 𝑋) ∧ 𝑞𝐴 ∧ (𝑃 < (𝑃(join‘𝐾)𝑞) ∧ (𝑃(join‘𝐾)𝑞)(le‘𝐾)𝑋)) → 𝐾 ∈ Lat)
2611, 3syl 17 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑋𝐵) ∧ 𝑃 < 𝑋) ∧ 𝑞𝐴 ∧ (𝑃 < (𝑃(join‘𝐾)𝑞) ∧ (𝑃(join‘𝐾)𝑞)(le‘𝐾)𝑋)) → 𝑃𝐵)
271, 2atbase 34095 . . . . . . . . 9 (𝑞𝐴𝑞𝐵)
28273ad2ant2 1081 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑋𝐵) ∧ 𝑃 < 𝑋) ∧ 𝑞𝐴 ∧ (𝑃 < (𝑃(join‘𝐾)𝑞) ∧ (𝑃(join‘𝐾)𝑞)(le‘𝐾)𝑋)) → 𝑞𝐵)
291, 6latjcom 16999 . . . . . . . 8 ((𝐾 ∈ Lat ∧ 𝑃𝐵𝑞𝐵) → (𝑃(join‘𝐾)𝑞) = (𝑞(join‘𝐾)𝑃))
3025, 26, 28, 29syl3anc 1323 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑋𝐵) ∧ 𝑃 < 𝑋) ∧ 𝑞𝐴 ∧ (𝑃 < (𝑃(join‘𝐾)𝑞) ∧ (𝑃(join‘𝐾)𝑞)(le‘𝐾)𝑋)) → (𝑃(join‘𝐾)𝑞) = (𝑞(join‘𝐾)𝑃))
3123, 30breqtrrd 4651 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑋𝐵) ∧ 𝑃 < 𝑋) ∧ 𝑞𝐴 ∧ (𝑃 < (𝑃(join‘𝐾)𝑞) ∧ (𝑃(join‘𝐾)𝑞)(le‘𝐾)𝑋)) → 𝑞 < (𝑃(join‘𝐾)𝑞))
32 simp3r 1088 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑋𝐵) ∧ 𝑃 < 𝑋) ∧ 𝑞𝐴 ∧ (𝑃 < (𝑃(join‘𝐾)𝑞) ∧ (𝑃(join‘𝐾)𝑞)(le‘𝐾)𝑋)) → (𝑃(join‘𝐾)𝑞)(le‘𝐾)𝑋)
33 hlpos 34171 . . . . . . . 8 (𝐾 ∈ HL → 𝐾 ∈ Poset)
3410, 33syl 17 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑋𝐵) ∧ 𝑃 < 𝑋) ∧ 𝑞𝐴 ∧ (𝑃 < (𝑃(join‘𝐾)𝑞) ∧ (𝑃(join‘𝐾)𝑞)(le‘𝐾)𝑋)) → 𝐾 ∈ Poset)
351, 6latjcl 16991 . . . . . . . 8 ((𝐾 ∈ Lat ∧ 𝑃𝐵𝑞𝐵) → (𝑃(join‘𝐾)𝑞) ∈ 𝐵)
3625, 26, 28, 35syl3anc 1323 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑋𝐵) ∧ 𝑃 < 𝑋) ∧ 𝑞𝐴 ∧ (𝑃 < (𝑃(join‘𝐾)𝑞) ∧ (𝑃(join‘𝐾)𝑞)(le‘𝐾)𝑋)) → (𝑃(join‘𝐾)𝑞) ∈ 𝐵)
37 simp1l3 1154 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑋𝐵) ∧ 𝑃 < 𝑋) ∧ 𝑞𝐴 ∧ (𝑃 < (𝑃(join‘𝐾)𝑞) ∧ (𝑃(join‘𝐾)𝑞)(le‘𝐾)𝑋)) → 𝑋𝐵)
381, 4, 5pltletr 16911 . . . . . . 7 ((𝐾 ∈ Poset ∧ (𝑞𝐵 ∧ (𝑃(join‘𝐾)𝑞) ∈ 𝐵𝑋𝐵)) → ((𝑞 < (𝑃(join‘𝐾)𝑞) ∧ (𝑃(join‘𝐾)𝑞)(le‘𝐾)𝑋) → 𝑞 < 𝑋))
3934, 28, 36, 37, 38syl13anc 1325 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑋𝐵) ∧ 𝑃 < 𝑋) ∧ 𝑞𝐴 ∧ (𝑃 < (𝑃(join‘𝐾)𝑞) ∧ (𝑃(join‘𝐾)𝑞)(le‘𝐾)𝑋)) → ((𝑞 < (𝑃(join‘𝐾)𝑞) ∧ (𝑃(join‘𝐾)𝑞)(le‘𝐾)𝑋) → 𝑞 < 𝑋))
4031, 32, 39mp2and 714 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑋𝐵) ∧ 𝑃 < 𝑋) ∧ 𝑞𝐴 ∧ (𝑃 < (𝑃(join‘𝐾)𝑞) ∧ (𝑃(join‘𝐾)𝑞)(le‘𝐾)𝑋)) → 𝑞 < 𝑋)
4120, 40jca 554 . . . 4 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑋𝐵) ∧ 𝑃 < 𝑋) ∧ 𝑞𝐴 ∧ (𝑃 < (𝑃(join‘𝐾)𝑞) ∧ (𝑃(join‘𝐾)𝑞)(le‘𝐾)𝑋)) → (𝑞𝑃𝑞 < 𝑋))
42413exp 1261 . . 3 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑋𝐵) ∧ 𝑃 < 𝑋) → (𝑞𝐴 → ((𝑃 < (𝑃(join‘𝐾)𝑞) ∧ (𝑃(join‘𝐾)𝑞)(le‘𝐾)𝑋) → (𝑞𝑃𝑞 < 𝑋))))
4342reximdvai 3011 . 2 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑋𝐵) ∧ 𝑃 < 𝑋) → (∃𝑞𝐴 (𝑃 < (𝑃(join‘𝐾)𝑞) ∧ (𝑃(join‘𝐾)𝑞)(le‘𝐾)𝑋) → ∃𝑞𝐴 (𝑞𝑃𝑞 < 𝑋)))
448, 43mpd 15 1 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑋𝐵) ∧ 𝑃 < 𝑋) → ∃𝑞𝐴 (𝑞𝑃𝑞 < 𝑋))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1036   = wceq 1480   ∈ wcel 1987   ≠ wne 2790  ∃wrex 2909   class class class wbr 4623  ‘cfv 5857  (class class class)co 6615  Basecbs 15800  lecple 15888  Posetcpo 16880  ltcplt 16881  joincjn 16884  Latclat 16985   ⋖ ccvr 34068  Atomscatm 34069  HLchlt 34156 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2913  df-rex 2914  df-reu 2915  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-op 4162  df-uni 4410  df-iun 4494  df-br 4624  df-opab 4684  df-mpt 4685  df-id 4999  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-riota 6576  df-ov 6618  df-oprab 6619  df-preset 16868  df-poset 16886  df-plt 16898  df-lub 16914  df-glb 16915  df-join 16916  df-meet 16917  df-p0 16979  df-lat 16986  df-clat 17048  df-oposet 33982  df-ol 33984  df-oml 33985  df-covers 34072  df-ats 34073  df-atl 34104  df-cvlat 34128  df-hlat 34157 This theorem is referenced by:  cdlemb  34599  lhpexle1  34813
 Copyright terms: Public domain W3C validator