This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ C ℋ
atabs.2 ⊢ B ∈ C ℋ
Assertion atabs2i ⊢ C ∈ HAtoms → ¬ C ⊆ A ∨ ℋ B → A ∨ ℋ C ∩ A ∨ ℋ B = A

Proof

Step Hyp Ref Expression
1 atabs.1 ⊢ A ∈ C ℋ
2 atabs.2 ⊢ B ∈ C ℋ
3 1 2 chjcli ⊢ A ∨ ℋ B ∈ C ℋ
4 1 3 atabsi ⊢ C ∈ HAtoms → ¬ C ⊆ A ∨ ℋ A ∨ ℋ B → A ∨ ℋ C ∩ A ∨ ℋ B = A ∩ A ∨ ℋ B
5 1 1 2 chjassi ⊢ A ∨ ℋ A ∨ ℋ B = A ∨ ℋ A ∨ ℋ B
6 1 chjidmi ⊢ A ∨ ℋ A = A
7 6 oveq1i ⊢ A ∨ ℋ A ∨ ℋ B = A ∨ ℋ B
8 5 7 eqtr3i ⊢ A ∨ ℋ A ∨ ℋ B = A ∨ ℋ B
9 8 sseq2i ⊢ C ⊆ A ∨ ℋ A ∨ ℋ B ↔ C ⊆ A ∨ ℋ B
10 9 notbii ⊢ ¬ C ⊆ A ∨ ℋ A ∨ ℋ B ↔ ¬ C ⊆ A ∨ ℋ B
11 1 2 chabs2i ⊢ A ∩ A ∨ ℋ B = A
12 11 eqeq2i ⊢ A ∨ ℋ C ∩ A ∨ ℋ B = A ∩ A ∨ ℋ B ↔ A ∨ ℋ C ∩ A ∨ ℋ B = A
13 4 10 12 3imtr3g ⊢ C ∈ HAtoms → ¬ C ⊆ A ∨ ℋ B → A ∨ ℋ C ∩ A ∨ ℋ B = A