Theorem cvmd

Description: The covering property implies the modular pair property. Lemma 7.5.1 of MaedaMaeda p. 31. (Contributed by NM, 21-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	cvmd	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge \left(A\cap B\right){⋖}_{\mathscr{H}}B\right)\to A{𝑀}_{\mathscr{H}}B$$

Proof

Step	Hyp	Ref	Expression
1		ineq1	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to A\cap B=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap B$$
2	1	breq1d	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to \left(\left(A\cap B\right){⋖}_{\mathscr{H}}B\leftrightarrow \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap B\right){⋖}_{\mathscr{H}}B\right)$$
3		breq1	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to \left(A{𝑀}_{\mathscr{H}}B\leftrightarrow if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){𝑀}_{\mathscr{H}}B\right)$$
4	2 3	imbi12d	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to \left(\left(\left(A\cap B\right){⋖}_{\mathscr{H}}B\to A{𝑀}_{\mathscr{H}}B\right)\leftrightarrow \left(\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap B\right){⋖}_{\mathscr{H}}B\to if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){𝑀}_{\mathscr{H}}B\right)\right)$$
5		ineq2	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap B=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)$$
6		id	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)$$
7	5 6	breq12d	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to \left(\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap B\right){⋖}_{\mathscr{H}}B\leftrightarrow \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right){⋖}_{\mathscr{H}}if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)$$
8		breq2	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){𝑀}_{\mathscr{H}}B\leftrightarrow if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){𝑀}_{\mathscr{H}}if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)$$
9	7 8	imbi12d	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to \left(\left(\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap B\right){⋖}_{\mathscr{H}}B\to if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){𝑀}_{\mathscr{H}}B\right)\leftrightarrow \left(\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right){⋖}_{\mathscr{H}}if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){𝑀}_{\mathscr{H}}if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)\right)$$
10		ifchhv	$$⊢if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
11		ifchhv	$$⊢if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
12	10 11	cvmdi	$$⊢\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right){⋖}_{\mathscr{H}}if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){𝑀}_{\mathscr{H}}if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)$$
13	4 9 12	dedth2h	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(A\cap B\right){⋖}_{\mathscr{H}}B\to A{𝑀}_{\mathscr{H}}B\right)$$
14	13	3impia	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge \left(A\cap B\right){⋖}_{\mathscr{H}}B\right)\to A{𝑀}_{\mathscr{H}}B$$