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

Theorem atlex 35204
Description: Every nonzero element of an atomic lattice is greater than or equal to an atom. (hatomic 29610 analog.) (Contributed by NM, 21-Oct-2011.)
Hypotheses
Ref Expression
atlex.b 𝐵 = (Base‘𝐾)
atlex.l = (le‘𝐾)
atlex.z 0 = (0.‘𝐾)
atlex.a 𝐴 = (Atoms‘𝐾)
Assertion
Ref Expression
atlex ((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑋0 ) → ∃𝑦𝐴 𝑦 𝑋)
Distinct variable groups:   𝑦,𝐴   𝑦,𝐾   𝑦,𝑋
Allowed substitution hints:   𝐵(𝑦)   (𝑦)   0 (𝑦)

Proof of Theorem atlex
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 atlex.b . . . . 5 𝐵 = (Base‘𝐾)
2 eqid 2765 . . . . 5 (glb‘𝐾) = (glb‘𝐾)
3 atlex.l . . . . 5 = (le‘𝐾)
4 atlex.z . . . . 5 0 = (0.‘𝐾)
5 atlex.a . . . . 5 𝐴 = (Atoms‘𝐾)
61, 2, 3, 4, 5isatl 35187 . . . 4 (𝐾 ∈ AtLat ↔ (𝐾 ∈ Lat ∧ 𝐵 ∈ dom (glb‘𝐾) ∧ ∀𝑥𝐵 (𝑥0 → ∃𝑦𝐴 𝑦 𝑥)))
76simp3bi 1177 . . 3 (𝐾 ∈ AtLat → ∀𝑥𝐵 (𝑥0 → ∃𝑦𝐴 𝑦 𝑥))
8 neeq1 2999 . . . . 5 (𝑥 = 𝑋 → (𝑥0𝑋0 ))
9 breq2 4813 . . . . . 6 (𝑥 = 𝑋 → (𝑦 𝑥𝑦 𝑋))
109rexbidv 3199 . . . . 5 (𝑥 = 𝑋 → (∃𝑦𝐴 𝑦 𝑥 ↔ ∃𝑦𝐴 𝑦 𝑋))
118, 10imbi12d 335 . . . 4 (𝑥 = 𝑋 → ((𝑥0 → ∃𝑦𝐴 𝑦 𝑥) ↔ (𝑋0 → ∃𝑦𝐴 𝑦 𝑋)))
1211rspccv 3458 . . 3 (∀𝑥𝐵 (𝑥0 → ∃𝑦𝐴 𝑦 𝑥) → (𝑋𝐵 → (𝑋0 → ∃𝑦𝐴 𝑦 𝑋)))
137, 12syl 17 . 2 (𝐾 ∈ AtLat → (𝑋𝐵 → (𝑋0 → ∃𝑦𝐴 𝑦 𝑋)))
14133imp 1137 1 ((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑋0 ) → ∃𝑦𝐴 𝑦 𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1107   = wceq 1652  wcel 2155  wne 2937  wral 3055  wrex 3056   class class class wbr 4809  dom cdm 5277  cfv 6068  Basecbs 16132  lecple 16223  glbcglb 17211  0.cp0 17305  Latclat 17313  Atomscatm 35151  AtLatcal 35152
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-br 4810  df-dm 5287  df-iota 6031  df-fv 6076  df-atl 35186
This theorem is referenced by:  atnle  35205  atlatmstc  35207  cvratlem  35309  cvrat4  35331  2llnmat  35412  2lnat  35672
  Copyright terms: Public domain W3C validator