![]() |
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 4334 | . . . 4 β’ (π β π β Β¬ π = β ) | |
2 | llnbase.n | . . . . 5 β’ π = (LLinesβπΎ) | |
3 | 2 | eqeq1i 2738 | . . . 4 β’ (π = β β (LLinesβπΎ) = β ) |
4 | 1, 3 | sylnib 328 | . . 3 β’ (π β π β Β¬ (LLinesβπΎ) = β ) |
5 | fvprc 6884 | . . 3 β’ (Β¬ πΎ β V β (LLinesβπΎ) = β ) | |
6 | 4, 5 | nsyl2 141 | . 2 β’ (π β π β πΎ β V) |
7 | llnbase.b | . . . 4 β’ π΅ = (BaseβπΎ) | |
8 | eqid 2733 | . . . 4 β’ ( β βπΎ) = ( β βπΎ) | |
9 | eqid 2733 | . . . 4 β’ (AtomsβπΎ) = (AtomsβπΎ) | |
10 | 7, 8, 9, 2 | islln 38377 | . . 3 β’ (πΎ β V β (π β π β (π β π΅ β§ βπ β (AtomsβπΎ)π( β βπΎ)π))) |
11 | 10 | simprbda 500 | . 2 β’ ((πΎ β V β§ π β π) β π β π΅) |
12 | 6, 11 | mpancom 687 | 1 β’ (π β π β π β π΅) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 = wceq 1542 β wcel 2107 βwrex 3071 Vcvv 3475 β c0 4323 class class class wbr 5149 βcfv 6544 Basecbs 17144 β ccvr 38132 Atomscatm 38133 LLinesclln 38362 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pr 5428 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-iota 6496 df-fun 6546 df-fv 6552 df-llines 38369 |
This theorem is referenced by: islln2 38382 llnnleat 38384 llnneat 38385 atcvrlln2 38390 llnexatN 38392 llncmp 38393 2llnmat 38395 islpln3 38404 llnmlplnN 38410 lplnle 38411 lplnnle2at 38412 llncvrlpln2 38428 llncvrlpln 38429 2llnmj 38431 lplncmp 38433 lplnexatN 38434 lplnexllnN 38435 2llnm2N 38439 2llnm3N 38440 2llnm4 38441 2llnmeqat 38442 dalem21 38565 dalem54 38597 dalem55 38598 dalem57 38600 dalem60 38603 llnexchb2lem 38739 llnexchb2 38740 llnexch2N 38741 |
Copyright terms: Public domain | W3C validator |