Metamath Proof Explorer


Theorem atabsi

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 AC
atabs.2 BC
Assertion atabsi CHAtoms¬CABACB=AB

Proof

Step Hyp Ref Expression
1 atabs.1 AC
2 atabs.2 BC
3 inass ACABB=ACABB
4 1 2 chjcomi AB=BA
5 4 ineq1i ABB=BAB
6 incom BAB=BBA
7 2 1 chabs2i BBA=B
8 5 6 7 3eqtri ABB=B
9 8 ineq2i ACABB=ACB
10 3 9 eqtr2i ACB=ACABB
11 1 2 chub1i AAB
12 atelch CHAtomsCC
13 1 2 chjcli ABC
14 atmd CHAtomsABCC𝑀AB
15 13 14 mpan2 CHAtomsC𝑀AB
16 mdi CCABCACC𝑀ABAABACAB=ACAB
17 16 exp32 CCABCACC𝑀ABAABACAB=ACAB
18 13 1 17 mp3an23 CCC𝑀ABAABACAB=ACAB
19 12 15 18 sylc CHAtomsAABACAB=ACAB
20 11 19 mpi CHAtomsACAB=ACAB
21 20 adantr CHAtoms¬CABACAB=ACAB
22 incom CAB=ABC
23 atnssm0 ABCCHAtoms¬CABABC=0
24 13 23 mpan CHAtoms¬CABABC=0
25 24 biimpa CHAtoms¬CABABC=0
26 22 25 eqtrid CHAtoms¬CABCAB=0
27 26 oveq2d CHAtoms¬CABACAB=A0
28 1 chj0i A0=A
29 27 28 eqtrdi CHAtoms¬CABACAB=A
30 21 29 eqtrd CHAtoms¬CABACAB=A
31 30 ineq1d CHAtoms¬CABACABB=AB
32 10 31 eqtrid CHAtoms¬CABACB=AB
33 32 ex CHAtoms¬CABACB=AB