Description: Absorption of an incomparable atom. Similar to Exercise 7.1 of MaedaMaeda p. 34. (Contributed by NM, 15-Jul-2004) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | atabs.1 | |
|
atabs.2 | |
||
Assertion | atabsi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | atabs.1 | |
|
2 | atabs.2 | |
|
3 | inass | |
|
4 | 1 2 | chjcomi | |
5 | 4 | ineq1i | |
6 | incom | |
|
7 | 2 1 | chabs2i | |
8 | 5 6 7 | 3eqtri | |
9 | 8 | ineq2i | |
10 | 3 9 | eqtr2i | |
11 | 1 2 | chub1i | |
12 | atelch | |
|
13 | 1 2 | chjcli | |
14 | atmd | |
|
15 | 13 14 | mpan2 | |
16 | mdi | |
|
17 | 16 | exp32 | |
18 | 13 1 17 | mp3an23 | |
19 | 12 15 18 | sylc | |
20 | 11 19 | mpi | |
21 | 20 | adantr | |
22 | incom | |
|
23 | atnssm0 | |
|
24 | 13 23 | mpan | |
25 | 24 | biimpa | |
26 | 22 25 | eqtrid | |
27 | 26 | oveq2d | |
28 | 1 | chj0i | |
29 | 27 28 | eqtrdi | |
30 | 21 29 | eqtrd | |
31 | 30 | ineq1d | |
32 | 10 31 | eqtrid | |
33 | 32 | ex | |