# Metamath Proof Explorer

## Theorem atabs2i

Description: Absorption of an incomparable atom. (Contributed by NM, 18-Jul-2004) (New usage is discouraged.)

Ref Expression
Hypotheses atabs.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
atabs.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
Assertion atabs2i ${⊢}{C}\in \mathrm{HAtoms}\to \left(¬{C}\subseteq {A}{\vee }_{ℋ}{B}\to \left({A}{\vee }_{ℋ}{C}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)={A}\right)$

### Proof

Step Hyp Ref Expression
1 atabs.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
2 atabs.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
3 1 2 chjcli ${⊢}{A}{\vee }_{ℋ}{B}\in {\mathbf{C}}_{ℋ}$
4 1 3 atabsi ${⊢}{C}\in \mathrm{HAtoms}\to \left(¬{C}\subseteq {A}{\vee }_{ℋ}\left({A}{\vee }_{ℋ}{B}\right)\to \left({A}{\vee }_{ℋ}{C}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)={A}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)$
5 1 1 2 chjassi ${⊢}\left({A}{\vee }_{ℋ}{A}\right){\vee }_{ℋ}{B}={A}{\vee }_{ℋ}\left({A}{\vee }_{ℋ}{B}\right)$
6 1 chjidmi ${⊢}{A}{\vee }_{ℋ}{A}={A}$
7 6 oveq1i ${⊢}\left({A}{\vee }_{ℋ}{A}\right){\vee }_{ℋ}{B}={A}{\vee }_{ℋ}{B}$
8 5 7 eqtr3i ${⊢}{A}{\vee }_{ℋ}\left({A}{\vee }_{ℋ}{B}\right)={A}{\vee }_{ℋ}{B}$
9 8 sseq2i ${⊢}{C}\subseteq {A}{\vee }_{ℋ}\left({A}{\vee }_{ℋ}{B}\right)↔{C}\subseteq {A}{\vee }_{ℋ}{B}$
10 9 notbii ${⊢}¬{C}\subseteq {A}{\vee }_{ℋ}\left({A}{\vee }_{ℋ}{B}\right)↔¬{C}\subseteq {A}{\vee }_{ℋ}{B}$
11 1 2 chabs2i ${⊢}{A}\cap \left({A}{\vee }_{ℋ}{B}\right)={A}$
12 11 eqeq2i ${⊢}\left({A}{\vee }_{ℋ}{C}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)={A}\cap \left({A}{\vee }_{ℋ}{B}\right)↔\left({A}{\vee }_{ℋ}{C}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)={A}$
13 4 10 12 3imtr3g ${⊢}{C}\in \mathrm{HAtoms}\to \left(¬{C}\subseteq {A}{\vee }_{ℋ}{B}\to \left({A}{\vee }_{ℋ}{C}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)={A}\right)$