Theorem cmbr4i

Description: Alternate definition for the commutes relation. (Contributed by NM, 6-Dec-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjoml2.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	pjoml2.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	cmbr4i	$$⊢A{𝐶}_{\mathscr{H}}B\leftrightarrow A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		pjoml2.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjoml2.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3	1 2	cmbr3i	$$⊢A{𝐶}_{\mathscr{H}}B\leftrightarrow A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)=A\cap B$$
4		inss2	$$⊢A\cap B\subseteq B$$
5		sseq1	$$⊢A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)=A\cap B\to \left(A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)\subseteq B\leftrightarrow A\cap B\subseteq B\right)$$
6	4 5	mpbiri	$$⊢A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)=A\cap B\to A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)\subseteq B$$
7		inss1	$$⊢A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)\subseteq A$$
8	7	jctl	$$⊢A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)\subseteq B\to \left(A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)\subseteq A\wedge A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)\subseteq B\right)$$
9		ssin	$$⊢\left(A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)\subseteq A\wedge A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)\subseteq B\right)\leftrightarrow A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)\subseteq A\cap B$$
10	8 9	sylib	$$⊢A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)\subseteq B\to A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)\subseteq A\cap B$$
11	1	choccli	$$⊢\perp \left(A\right)\in {\mathbf{C}}_{\mathscr{H}}$$
12	2 11	chub2i	$$⊢B\subseteq \perp \left(A\right){\vee }_{\mathscr{H}}B$$
13		sslin	$$⊢B\subseteq \perp \left(A\right){\vee }_{\mathscr{H}}B\to A\cap B\subseteq A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)$$
14	12 13	ax-mp	$$⊢A\cap B\subseteq A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)$$
15	10 14	jctir	$$⊢A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)\subseteq B\to \left(A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)\subseteq A\cap B\wedge A\cap B\subseteq A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)\right)$$
16		eqss	$$⊢A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)=A\cap B\leftrightarrow \left(A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)\subseteq A\cap B\wedge A\cap B\subseteq A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)\right)$$
17	15 16	sylibr	$$⊢A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)\subseteq B\to A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)=A\cap B$$
18	6 17	impbii	$$⊢A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)=A\cap B\leftrightarrow A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)\subseteq B$$
19	3 18	bitri	$$⊢A{𝐶}_{\mathscr{H}}B\leftrightarrow A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)\subseteq B$$