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 ⊢ 𝐴 ∈ Cℋ
atabs.2 ⊢ 𝐵 ∈ Cℋ
Assertion atabs2i ( 𝐶 ∈ HAtoms → ( ¬ 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = 𝐴 ) )

Proof

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