Description: The meet of two intersecting lines (expressed as joins of atoms) is an atom. (Contributed by NM, 21-Nov-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | 2atmat.l | |
|
2atmat.j | |
||
2atmat.m | |
||
2atmat.a | |
||
Assertion | 2atmat | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2atmat.l | |
|
2 | 2atmat.j | |
|
3 | 2atmat.m | |
|
4 | 2atmat.a | |
|
5 | simp11 | |
|
6 | 5 | hllatd | |
7 | eqid | |
|
8 | 7 2 4 | hlatjcl | |
9 | 8 | 3ad2ant1 | |
10 | simp21 | |
|
11 | 7 4 | atbase | |
12 | 10 11 | syl | |
13 | simp22 | |
|
14 | 7 4 | atbase | |
15 | 13 14 | syl | |
16 | 7 2 | latjass | |
17 | 6 9 12 15 16 | syl13anc | |
18 | simp33 | |
|
19 | 7 2 | latjcl | |
20 | 6 9 12 19 | syl3anc | |
21 | 7 1 2 | latleeqj2 | |
22 | 6 15 20 21 | syl3anc | |
23 | 18 22 | mpbid | |
24 | 17 23 | eqtr3d | |
25 | simp23 | |
|
26 | simp32 | |
|
27 | simp12 | |
|
28 | simp13 | |
|
29 | eqid | |
|
30 | 1 2 4 29 | islpln2a | |
31 | 5 27 28 10 30 | syl13anc | |
32 | 25 26 31 | mpbir2and | |
33 | 24 32 | eqeltrd | |
34 | eqid | |
|
35 | 2 4 34 | llni2 | |
36 | 5 27 28 25 35 | syl31anc | |
37 | simp31 | |
|
38 | 2 4 34 | llni2 | |
39 | 5 10 13 37 38 | syl31anc | |
40 | 2 3 4 34 29 | 2llnmj | |
41 | 5 36 39 40 | syl3anc | |
42 | 33 41 | mpbird | |