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

Theorem atcvrlln 33048
 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 1045 . . 3
2 simpll3 1047 . . 3
3 simpr 463 . . 3
4 simplr 761 . . 3
5 atcvrlln.b . . . 4
6 atcvrlln.c . . . 4
7 atcvrlln.a . . . 4
8 atcvrlln.n . . . 4
95, 6, 7, 8llni 33036 . . 3
101, 2, 3, 4, 9syl31anc 1268 . 2
11 simpr 463 . . . 4
12 simpll1 1045 . . . . 5
13 simpll3 1047 . . . . 5
14 eqid 2423 . . . . . 6
155, 14, 7, 8islln3 33038 . . . . 5
1612, 13, 15syl2anc 666 . . . 4
1711, 16mpbid 214 . . 3
18 simp1l1 1099 . . . . . . 7
19 simp1l2 1100 . . . . . . 7
20 simp2l 1032 . . . . . . 7
21 simp2r 1033 . . . . . . 7
22 simp3l 1034 . . . . . . 7
23 simp1r 1031 . . . . . . . 8
24 simp3r 1035 . . . . . . . 8
2523, 24breqtrd 4446 . . . . . . 7
265, 14, 6, 7cvrat2 32957 . . . . . . 7
2718, 19, 20, 21, 22, 25, 26syl132anc 1283 . . . . . 6
28273exp 1205 . . . . 5
2928rexlimdvv 2924 . . . 4