![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > llnbase | Structured version Visualization version Unicode version |
Description: A lattice line is a lattice element. (Contributed by NM, 16-Jun-2012.) |
Ref | Expression |
---|---|
llnbase.b |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
llnbase.n |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
llnbase |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | n0i 3748 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | llnbase.n |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | eqeq1i 2467 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | sylnib 310 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | fvprc 5882 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 4, 5 | nsyl2 132 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | llnbase.b |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | eqid 2462 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | eqid 2462 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
10 | 7, 8, 9, 2 | islln 33116 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 10 | simprbda 633 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | 6, 11 | mpancom 680 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-8 1900 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-sep 4539 ax-nul 4548 ax-pow 4595 ax-pr 4653 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-ral 2754 df-rex 2755 df-rab 2758 df-v 3059 df-sbc 3280 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-nul 3744 df-if 3894 df-sn 3981 df-pr 3983 df-op 3987 df-uni 4213 df-br 4417 df-opab 4476 df-mpt 4477 df-id 4768 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-iota 5565 df-fun 5603 df-fv 5609 df-llines 33108 |
This theorem is referenced by: islln2 33121 llnnleat 33123 llnneat 33124 atcvrlln2 33129 llnexatN 33131 llncmp 33132 2llnmat 33134 islpln3 33143 llnmlplnN 33149 lplnle 33150 lplnnle2at 33151 llncvrlpln2 33167 llncvrlpln 33168 2llnmj 33170 lplncmp 33172 lplnexatN 33173 lplnexllnN 33174 2llnm2N 33178 2llnm3N 33179 2llnm4 33180 2llnmeqat 33181 dalem21 33304 dalem54 33336 dalem55 33337 dalem57 33339 dalem60 33342 llnexchb2lem 33478 llnexchb2 33479 llnexch2N 33480 |
Copyright terms: Public domain | W3C validator |