Theorem cvmdi

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

	Ref	Expression
Hypotheses	mdsl.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	mdsl.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	cvmdi	$$⊢\left(A\cap B\right){⋖}_{\mathscr{H}}B\to A{𝑀}_{\mathscr{H}}B$$

Proof

Step	Hyp	Ref	Expression
1		mdsl.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		mdsl.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3		anass	$$⊢\left(\left(A\cap B\subseteq x\wedge x\subseteq A{\vee }_{\mathscr{H}}B\right)\wedge x\subseteq B\right)\leftrightarrow \left(A\cap B\subseteq x\wedge \left(x\subseteq A{\vee }_{\mathscr{H}}B\wedge x\subseteq B\right)\right)$$
4	2 1	chub2i	$$⊢B\subseteq A{\vee }_{\mathscr{H}}B$$
5		sstr	$$⊢\left(x\subseteq B\wedge B\subseteq A{\vee }_{\mathscr{H}}B\right)\to x\subseteq A{\vee }_{\mathscr{H}}B$$
6	4 5	mpan2	$$⊢x\subseteq B\to x\subseteq A{\vee }_{\mathscr{H}}B$$
7	6	pm4.71ri	$$⊢x\subseteq B\leftrightarrow \left(x\subseteq A{\vee }_{\mathscr{H}}B\wedge x\subseteq B\right)$$
8	7	anbi2i	$$⊢\left(A\cap B\subseteq x\wedge x\subseteq B\right)\leftrightarrow \left(A\cap B\subseteq x\wedge \left(x\subseteq A{\vee }_{\mathscr{H}}B\wedge x\subseteq B\right)\right)$$
9	3 8	bitr4i	$$⊢\left(\left(A\cap B\subseteq x\wedge x\subseteq A{\vee }_{\mathscr{H}}B\right)\wedge x\subseteq B\right)\leftrightarrow \left(A\cap B\subseteq x\wedge x\subseteq B\right)$$
10	1 2	chincli	$$⊢A\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
11		cvnbtwn4	$$⊢\left(A\cap B\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(A\cap B\right){⋖}_{\mathscr{H}}B\to \left(\left(A\cap B\subseteq x\wedge x\subseteq B\right)\to \left(x=A\cap B\vee x=B\right)\right)\right)$$
12	10 2 11	mp3an12	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\left(A\cap B\right){⋖}_{\mathscr{H}}B\to \left(\left(A\cap B\subseteq x\wedge x\subseteq B\right)\to \left(x=A\cap B\vee x=B\right)\right)\right)$$
13	12	impcom	$$⊢\left(\left(A\cap B\right){⋖}_{\mathscr{H}}B\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(A\cap B\subseteq x\wedge x\subseteq B\right)\to \left(x=A\cap B\vee x=B\right)\right)$$
14	10 1	chjcomi	$$⊢\left(A\cap B\right){\vee }_{\mathscr{H}}A=A{\vee }_{\mathscr{H}}\left(A\cap B\right)$$
15	1 2	chabs1i	$$⊢A{\vee }_{\mathscr{H}}\left(A\cap B\right)=A$$
16	14 15	eqtri	$$⊢\left(A\cap B\right){\vee }_{\mathscr{H}}A=A$$
17	16	ineq1i	$$⊢\left(\left(A\cap B\right){\vee }_{\mathscr{H}}A\right)\cap B=A\cap B$$
18	10	chjidmi	$$⊢\left(A\cap B\right){\vee }_{\mathscr{H}}\left(A\cap B\right)=A\cap B$$
19	17 18	eqtr4i	$$⊢\left(\left(A\cap B\right){\vee }_{\mathscr{H}}A\right)\cap B=\left(A\cap B\right){\vee }_{\mathscr{H}}\left(A\cap B\right)$$
20		oveq1	$$⊢x=A\cap B\to x{\vee }_{\mathscr{H}}A=\left(A\cap B\right){\vee }_{\mathscr{H}}A$$
21	20	ineq1d	$$⊢x=A\cap B\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=\left(\left(A\cap B\right){\vee }_{\mathscr{H}}A\right)\cap B$$
22		oveq1	$$⊢x=A\cap B\to x{\vee }_{\mathscr{H}}\left(A\cap B\right)=\left(A\cap B\right){\vee }_{\mathscr{H}}\left(A\cap B\right)$$
23	19 21 22	3eqtr4a	$$⊢x=A\cap B\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)$$
24		incom	$$⊢\left(B{\vee }_{\mathscr{H}}A\right)\cap B=B\cap \left(B{\vee }_{\mathscr{H}}A\right)$$
25	2 1	chabs2i	$$⊢B\cap \left(B{\vee }_{\mathscr{H}}A\right)=B$$
26	2 1	chabs1i	$$⊢B{\vee }_{\mathscr{H}}\left(B\cap A\right)=B$$
27		incom	$$⊢B\cap A=A\cap B$$
28	27	oveq2i	$$⊢B{\vee }_{\mathscr{H}}\left(B\cap A\right)=B{\vee }_{\mathscr{H}}\left(A\cap B\right)$$
29	25 26 28	3eqtr2i	$$⊢B\cap \left(B{\vee }_{\mathscr{H}}A\right)=B{\vee }_{\mathscr{H}}\left(A\cap B\right)$$
30	24 29	eqtri	$$⊢\left(B{\vee }_{\mathscr{H}}A\right)\cap B=B{\vee }_{\mathscr{H}}\left(A\cap B\right)$$
31		oveq1	$$⊢x=B\to x{\vee }_{\mathscr{H}}A=B{\vee }_{\mathscr{H}}A$$
32	31	ineq1d	$$⊢x=B\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=\left(B{\vee }_{\mathscr{H}}A\right)\cap B$$
33		oveq1	$$⊢x=B\to x{\vee }_{\mathscr{H}}\left(A\cap B\right)=B{\vee }_{\mathscr{H}}\left(A\cap B\right)$$
34	30 32 33	3eqtr4a	$$⊢x=B\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)$$
35	23 34	jaoi	$$⊢\left(x=A\cap B\vee x=B\right)\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)$$
36	13 35	syl6	$$⊢\left(\left(A\cap B\right){⋖}_{\mathscr{H}}B\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(A\cap B\subseteq x\wedge x\subseteq B\right)\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)$$
37	9 36	syl5bi	$$⊢\left(\left(A\cap B\right){⋖}_{\mathscr{H}}B\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(\left(A\cap B\subseteq x\wedge x\subseteq A{\vee }_{\mathscr{H}}B\right)\wedge x\subseteq B\right)\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)$$
38	37	exp4b	$$⊢\left(A\cap B\right){⋖}_{\mathscr{H}}B\to \left(x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\left(A\cap B\subseteq x\wedge x\subseteq A{\vee }_{\mathscr{H}}B\right)\to \left(x\subseteq B\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\right)\right)$$
39	38	ralrimiv	$$⊢\left(A\cap B\right){⋖}_{\mathscr{H}}B\to \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(\left(A\cap B\subseteq x\wedge x\subseteq A{\vee }_{\mathscr{H}}B\right)\to \left(x\subseteq B\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\right)$$
40	1 2	mdsl1i	$$⊢\forall x\in {\mathbf{C}}_{\mathscr{H}}\left(\left(A\cap B\subseteq x\wedge x\subseteq A{\vee }_{\mathscr{H}}B\right)\to \left(x\subseteq B\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\right)\leftrightarrow A{𝑀}_{\mathscr{H}}B$$
41	39 40	sylib	$$⊢\left(A\cap B\right){⋖}_{\mathscr{H}}B\to A{𝑀}_{\mathscr{H}}B$$