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 → ( ¬ 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = 𝐴 ) )