Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  atcvrlln Unicode version

Theorem atcvrlln 30002
 Description: An element covering an atom is a lattice line and vice-versa. (Contributed by NM, 18-Jun-2012.)
Hypotheses
Ref Expression
atcvrlln.b
atcvrlln.c
atcvrlln.a
atcvrlln.n
Assertion
Ref Expression
atcvrlln

Proof of Theorem atcvrlln
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpll1 996 . . 3
2 simpll3 998 . . 3
3 simpr 448 . . 3
4 simplr 732 . . 3
5 atcvrlln.b . . . 4
6 atcvrlln.c . . . 4
7 atcvrlln.a . . . 4
8 atcvrlln.n . . . 4
95, 6, 7, 8llni 29990 . . 3
101, 2, 3, 4, 9syl31anc 1187 . 2
11 simpr 448 . . . 4
12 simpll1 996 . . . . 5
13 simpll3 998 . . . . 5
14 eqid 2404 . . . . . 6
155, 14, 7, 8islln3 29992 . . . . 5
1612, 13, 15syl2anc 643 . . . 4
1711, 16mpbid 202 . . 3
18 simp1l1 1050 . . . . . . 7
19 simp1l2 1051 . . . . . . 7
20 simp2l 983 . . . . . . 7
21 simp2r 984 . . . . . . 7
22 simp3l 985 . . . . . . 7
23 simp1r 982 . . . . . . . 8
24 simp3r 986 . . . . . . . 8
2523, 24breqtrd 4196 . . . . . . 7
265, 14, 6, 7cvrat2 29911 . . . . . . 7
2718, 19, 20, 21, 22, 25, 26syl132anc 1202 . . . . . 6
28273exp 1152 . . . . 5
2928rexlimdvv 2796 . . . 4