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

Theorem intnatN 32941
 Description: If the intersection with a non-majorizing element is an atom, the intersecting element is not an atom. (Contributed by NM, 26-Jun-2012.) (New usage is discouraged.)
Hypotheses
Ref Expression
intnat.b
intnat.l
intnat.m
intnat.a
Assertion
Ref Expression
intnatN

Proof of Theorem intnatN
StepHypRef Expression
1 hlatl 32895 . . . . . . 7
213ad2ant1 1026 . . . . . 6
32ad2antrr 730 . . . . 5
4 eqid 2422 . . . . . 6
5 intnat.a . . . . . 6
64, 5atn0 32843 . . . . 5
73, 6sylancom 671 . . . 4
87ex 435 . . 3
9 simpll1 1044 . . . . . . . 8
10 hllat 32898 . . . . . . . 8
119, 10syl 17 . . . . . . 7
12 simpll2 1045 . . . . . . 7
13 simpll3 1046 . . . . . . 7
14 intnat.b . . . . . . . 8
15 intnat.m . . . . . . . 8
1614, 15latmcom 16320 . . . . . . 7
1711, 12, 13, 16syl3anc 1264 . . . . . 6
18 simplr 760 . . . . . . 7
199, 1syl 17 . . . . . . . 8
20 simpr 462 . . . . . . . 8
21 intnat.l . . . . . . . . 9
2214, 21, 15, 4, 5atnle 32852 . . . . . . . 8
2319, 20, 12, 22syl3anc 1264 . . . . . . 7
2418, 23mpbid 213 . . . . . 6
2517, 24eqtrd 2463 . . . . 5
2625ex 435 . . . 4