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}}_{\mathscr{H}}$$
	atabs.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	atabs2i	$$⊢C\in \mathrm{HAtoms}\to \left(\neg C\subseteq A{\vee }_{\mathscr{H}}B\to \left(A{\vee }_{\mathscr{H}}C\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)=A\right)$$

Proof

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