![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > llnbase | Structured version Visualization version GIF version |
Description: A lattice line is a lattice element. (Contributed by NM, 16-Jun-2012.) |
Ref | Expression |
---|---|
llnbase.b | ⊢ 𝐵 = (Base‘𝐾) |
llnbase.n | ⊢ 𝑁 = (LLines‘𝐾) |
Ref | Expression |
---|---|
llnbase | ⊢ (𝑋 ∈ 𝑁 → 𝑋 ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | n0i 4065 | . . . 4 ⊢ (𝑋 ∈ 𝑁 → ¬ 𝑁 = ∅) | |
2 | llnbase.n | . . . . 5 ⊢ 𝑁 = (LLines‘𝐾) | |
3 | 2 | eqeq1i 2774 | . . . 4 ⊢ (𝑁 = ∅ ↔ (LLines‘𝐾) = ∅) |
4 | 1, 3 | sylnib 317 | . . 3 ⊢ (𝑋 ∈ 𝑁 → ¬ (LLines‘𝐾) = ∅) |
5 | fvprc 6325 | . . 3 ⊢ (¬ 𝐾 ∈ V → (LLines‘𝐾) = ∅) | |
6 | 4, 5 | nsyl2 144 | . 2 ⊢ (𝑋 ∈ 𝑁 → 𝐾 ∈ V) |
7 | llnbase.b | . . . 4 ⊢ 𝐵 = (Base‘𝐾) | |
8 | eqid 2769 | . . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾) | |
9 | eqid 2769 | . . . 4 ⊢ (Atoms‘𝐾) = (Atoms‘𝐾) | |
10 | 7, 8, 9, 2 | islln 35314 | . . 3 ⊢ (𝐾 ∈ V → (𝑋 ∈ 𝑁 ↔ (𝑋 ∈ 𝐵 ∧ ∃𝑝 ∈ (Atoms‘𝐾)𝑝( ⋖ ‘𝐾)𝑋))) |
11 | 10 | simprbda 651 | . 2 ⊢ ((𝐾 ∈ V ∧ 𝑋 ∈ 𝑁) → 𝑋 ∈ 𝐵) |
12 | 6, 11 | mpancom 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 |