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

Theorem llnbase 35317
Description: A lattice line is a lattice element. (Contributed by NM, 16-Jun-2012.)
Hypotheses
Ref Expression
llnbase.b 𝐵 = (Base‘𝐾)
llnbase.n 𝑁 = (LLines‘𝐾)
Assertion
Ref Expression
llnbase (𝑋𝑁𝑋𝐵)

Proof of Theorem llnbase
Dummy variable 𝑝 is distinct from all other variables.
StepHypRef Expression
1 n0i 4065 . . . 4 (𝑋𝑁 → ¬ 𝑁 = ∅)
2 llnbase.n . . . . 5 𝑁 = (LLines‘𝐾)
32eqeq1i 2774 . . . 4 (𝑁 = ∅ ↔ (LLines‘𝐾) = ∅)
41, 3sylnib 317 . . 3 (𝑋𝑁 → ¬ (LLines‘𝐾) = ∅)
5 fvprc 6325 . . 3 𝐾 ∈ V → (LLines‘𝐾) = ∅)
64, 5nsyl2 144 . 2 (𝑋𝑁𝐾 ∈ V)
7 llnbase.b . . . 4 𝐵 = (Base‘𝐾)
8 eqid 2769 . . . 4 ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
9 eqid 2769 . . . 4 (Atoms‘𝐾) = (Atoms‘𝐾)
107, 8, 9, 2islln 35314 . . 3 (𝐾 ∈ V → (𝑋𝑁 ↔ (𝑋𝐵 ∧ ∃𝑝 ∈ (Atoms‘𝐾)𝑝( ⋖ ‘𝐾)𝑋)))
1110simprbda 651 . 2 ((𝐾 ∈ V ∧ 𝑋𝑁) → 𝑋𝐵)
126, 11mpancom 703 1 (𝑋𝑁𝑋𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1629  wcel 2143  wrex 3060  Vcvv 3348  c0 4060   class class class wbr 4783  cfv 6030  Basecbs 16070  ccvr 35071  Atomscatm 35072  LLinesclln 35299
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1868  ax-4 1883  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2145  ax-9 2152  ax-10 2172  ax-11 2188  ax-12 2201  ax-13 2406  ax-ext 2749  ax-sep 4911  ax-nul 4919  ax-pow 4970  ax-pr 5033
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1071  df-tru 1632  df-ex 1851  df-nf 1856  df-sb 2048  df-eu 2620  df-mo 2621  df-clab 2756  df-cleq 2762  df-clel 2765  df-nfc 2900  df-ral 3064  df-rex 3065  df-rab 3068  df-v 3350  df-sbc 3585  df-dif 3723  df-un 3725  df-in 3727  df-ss 3734  df-nul 4061  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4572  df-br 4784  df-opab 4844  df-mpt 4861  df-id 5156  df-xp 5254  df-rel 5255  df-cnv 5256  df-co 5257  df-dm 5258  df-iota 5993  df-fun 6032  df-fv 6038  df-llines 35306
This theorem is referenced by:  islln2  35319  llnnleat  35321  llnneat  35322  atcvrlln2  35327  llnexatN  35329  llncmp  35330  2llnmat  35332  islpln3  35341  llnmlplnN  35347  lplnle  35348  lplnnle2at  35349  llncvrlpln2  35365  llncvrlpln  35366  2llnmj  35368  lplncmp  35370  lplnexatN  35371  lplnexllnN  35372  2llnm2N  35376  2llnm3N  35377  2llnm4  35378  2llnmeqat  35379  dalem21  35502  dalem54  35534  dalem55  35535  dalem57  35537  dalem60  35540  llnexchb2lem  35676  llnexchb2  35677  llnexch2N  35678
  Copyright terms: Public domain W3C validator