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

Theorem exatleN 29593
 Description: A condition for an atom to be less than or equal to a lattice element. Part of proof of Lemma A in [Crawley] p. 112. (Contributed by NM, 28-Apr-2012.) (New usage is discouraged.)
Hypotheses
Ref Expression
atomle.b
atomle.l
atomle.j
atomle.a
Assertion
Ref Expression
exatleN

Proof of Theorem exatleN
StepHypRef Expression
1 simpl32 1037 . . . . 5
2 atomle.b . . . . . . 7
3 atomle.l . . . . . . 7
4 simp11l 1066 . . . . . . . 8
5 hllat 29553 . . . . . . . 8
64, 5syl 15 . . . . . . 7
7 simp122 1088 . . . . . . . 8
8 atomle.a . . . . . . . . 9
92, 8atbase 29479 . . . . . . . 8
107, 9syl 15 . . . . . . 7
11 simp121 1087 . . . . . . . . 9
122, 8atbase 29479 . . . . . . . . 9
1311, 12syl 15 . . . . . . . 8
14 simp123 1089 . . . . . . . . 9
152, 8atbase 29479 . . . . . . . . 9
1614, 15syl 15 . . . . . . . 8
17 atomle.j . . . . . . . . 9
182, 17latjcl 14156 . . . . . . . 8
196, 13, 16, 18syl3anc 1182 . . . . . . 7
20 simp11r 1067 . . . . . . 7
2114, 7, 113jca 1132 . . . . . . . . 9
22 simp2 956 . . . . . . . . 9
234, 21, 223jca 1132 . . . . . . . 8
24 simp133 1092 . . . . . . . 8
253, 17, 8hlatexch1 29584 . . . . . . . 8
2623, 24, 25sylc 56 . . . . . . 7
27 simp131 1090 . . . . . . . 8
28 simp3 957 . . . . . . . 8
292, 3, 17latjle12 14168 . . . . . . . . 9
306, 13, 16, 20, 29syl13anc 1184 . . . . . . . 8
3127, 28, 30mpbi2and 887 . . . . . . 7
322, 3, 6, 10, 19, 20, 26, 31lattrd 14164 . . . . . 6
33323expia 1153 . . . . 5
341, 33mtod 168 . . . 4
3534ex 423 . . 3