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 A C
atabs.2 B C
Assertion atabsi C HAtoms ¬ C A B A C B = A B

Proof

Step Hyp Ref Expression
1 atabs.1 A C
2 atabs.2 B C
3 inass A C A B B = A C A B B
4 1 2 chjcomi A B = B A
5 4 ineq1i A B B = B A B
6 incom B A B = B B A
7 2 1 chabs2i B B A = B
8 5 6 7 3eqtri A B B = B
9 8 ineq2i A C A B B = A C B
10 3 9 eqtr2i A C B = A C A B B
11 1 2 chub1i A A B
12 atelch C HAtoms C C
13 1 2 chjcli A B C
14 atmd C HAtoms A B C C 𝑀 A B
15 13 14 mpan2 C HAtoms C 𝑀 A B
16 mdi C C A B C A C C 𝑀 A B A A B A C A B = A C A B
17 16 exp32 C C A B C A C C 𝑀 A B A A B A C A B = A C A B
18 13 1 17 mp3an23 C C C 𝑀 A B A A B A C A B = A C A B
19 12 15 18 sylc C HAtoms A A B A C A B = A C A B
20 11 19 mpi C HAtoms A C A B = A C A B
21 20 adantr C HAtoms ¬ C A B A C A B = A C A B
22 incom C A B = A B C
23 atnssm0 A B C C HAtoms ¬ C A B A B C = 0
24 13 23 mpan C HAtoms ¬ C A B A B C = 0
25 24 biimpa C HAtoms ¬ C A B A B C = 0
26 22 25 syl5eq C HAtoms ¬ C A B C A B = 0
27 26 oveq2d C HAtoms ¬ C A B A C A B = A 0
28 1 chj0i A 0 = A
29 27 28 syl6eq C HAtoms ¬ C A B A C A B = A
30 21 29 eqtrd C HAtoms ¬ C A B A C A B = A
31 30 ineq1d C HAtoms ¬ C A B A C A B B = A B
32 10 31 syl5eq C HAtoms ¬ C A B A C B = A B
33 32 ex C HAtoms ¬ C A B A C B = A B