Theorem dmdbr5ati

Description: Dual modular pair property in terms of atoms. (Contributed by NM, 14-Jan-2005) (New usage is discouraged.)

	Ref	Expression
Hypotheses	sumdmdi.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	sumdmdi.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	dmdbr5ati	$$⊢A{𝑀}_{\mathscr{H}}^{*}B\leftrightarrow \forall x\in \mathrm{HAtoms}\left(x\subseteq A{\vee }_{\mathscr{H}}B\to x\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		sumdmdi.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		sumdmdi.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3		dmdi4	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{𝑀}_{\mathscr{H}}^{*}B\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)$$
4	1 2 3	mp3an12	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(A{𝑀}_{\mathscr{H}}^{*}B\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)$$
5		atelch	$$⊢x\in \mathrm{HAtoms}\to x\in {\mathbf{C}}_{\mathscr{H}}$$
6	4 5	syl11	$$⊢A{𝑀}_{\mathscr{H}}^{*}B\to \left(x\in \mathrm{HAtoms}\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)$$
7	6	a1dd	$$⊢A{𝑀}_{\mathscr{H}}^{*}B\to \left(x\in \mathrm{HAtoms}\to \left(x\subseteq A{\vee }_{\mathscr{H}}B\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)\right)$$
8	7	ralrimiv	$$⊢A{𝑀}_{\mathscr{H}}^{*}B\to \forall x\in \mathrm{HAtoms}\left(x\subseteq A{\vee }_{\mathscr{H}}B\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)$$
9		chjcom	$$⊢\left(B\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to B{\vee }_{\mathscr{H}}x=x{\vee }_{\mathscr{H}}B$$
10	2 5 9	sylancr	$$⊢x\in \mathrm{HAtoms}\to B{\vee }_{\mathscr{H}}x=x{\vee }_{\mathscr{H}}B$$
11	10	ineq1d	$$⊢x\in \mathrm{HAtoms}\to \left(B{\vee }_{\mathscr{H}}x\right)\cap \left(B{\vee }_{\mathscr{H}}A\right)=\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(B{\vee }_{\mathscr{H}}A\right)$$
12	1 2	chjcomi	$$⊢A{\vee }_{\mathscr{H}}B=B{\vee }_{\mathscr{H}}A$$
13	12	ineq2i	$$⊢\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)=\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(B{\vee }_{\mathscr{H}}A\right)$$
14	11 13	eqtr4di	$$⊢x\in \mathrm{HAtoms}\to \left(B{\vee }_{\mathscr{H}}x\right)\cap \left(B{\vee }_{\mathscr{H}}A\right)=\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)$$
15	14	adantr	$$⊢\left(x\in \mathrm{HAtoms}\wedge \neg x\subseteq A{\vee }_{\mathscr{H}}B\right)\to \left(B{\vee }_{\mathscr{H}}x\right)\cap \left(B{\vee }_{\mathscr{H}}A\right)=\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)$$
16	12	sseq2i	$$⊢x\subseteq A{\vee }_{\mathscr{H}}B\leftrightarrow x\subseteq B{\vee }_{\mathscr{H}}A$$
17	16	notbii	$$⊢\neg x\subseteq A{\vee }_{\mathscr{H}}B\leftrightarrow \neg x\subseteq B{\vee }_{\mathscr{H}}A$$
18	2 1	atabs2i	$$⊢x\in \mathrm{HAtoms}\to \left(\neg x\subseteq B{\vee }_{\mathscr{H}}A\to \left(B{\vee }_{\mathscr{H}}x\right)\cap \left(B{\vee }_{\mathscr{H}}A\right)=B\right)$$
19	18	imp	$$⊢\left(x\in \mathrm{HAtoms}\wedge \neg x\subseteq B{\vee }_{\mathscr{H}}A\right)\to \left(B{\vee }_{\mathscr{H}}x\right)\cap \left(B{\vee }_{\mathscr{H}}A\right)=B$$
20	17 19	sylan2b	$$⊢\left(x\in \mathrm{HAtoms}\wedge \neg x\subseteq A{\vee }_{\mathscr{H}}B\right)\to \left(B{\vee }_{\mathscr{H}}x\right)\cap \left(B{\vee }_{\mathscr{H}}A\right)=B$$
21	15 20	eqtr3d	$$⊢\left(x\in \mathrm{HAtoms}\wedge \neg x\subseteq A{\vee }_{\mathscr{H}}B\right)\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)=B$$
22		chjcl	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to x{\vee }_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}$$
23	5 2 22	sylancl	$$⊢x\in \mathrm{HAtoms}\to x{\vee }_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}$$
24		chincl	$$⊢\left(x{\vee }_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(x{\vee }_{\mathscr{H}}B\right)\cap A\in {\mathbf{C}}_{\mathscr{H}}$$
25	23 1 24	sylancl	$$⊢x\in \mathrm{HAtoms}\to \left(x{\vee }_{\mathscr{H}}B\right)\cap A\in {\mathbf{C}}_{\mathscr{H}}$$
26		chub2	$$⊢\left(B\in {\mathbf{C}}_{\mathscr{H}}\wedge \left(x{\vee }_{\mathscr{H}}B\right)\cap A\in {\mathbf{C}}_{\mathscr{H}}\right)\to B\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B$$
27	2 25 26	sylancr	$$⊢x\in \mathrm{HAtoms}\to B\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B$$
28	27	adantr	$$⊢\left(x\in \mathrm{HAtoms}\wedge \neg x\subseteq A{\vee }_{\mathscr{H}}B\right)\to B\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B$$
29	21 28	eqsstrd	$$⊢\left(x\in \mathrm{HAtoms}\wedge \neg x\subseteq A{\vee }_{\mathscr{H}}B\right)\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B$$
30	29	ex	$$⊢x\in \mathrm{HAtoms}\to \left(\neg x\subseteq A{\vee }_{\mathscr{H}}B\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)$$
31	30	biantrud	$$⊢x\in \mathrm{HAtoms}\to \left(\left(x\subseteq A{\vee }_{\mathscr{H}}B\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)\leftrightarrow \left(\left(x\subseteq A{\vee }_{\mathscr{H}}B\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)\wedge \left(\neg x\subseteq A{\vee }_{\mathscr{H}}B\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)\right)\right)$$
32		pm4.83	$$⊢\left(\left(x\subseteq A{\vee }_{\mathscr{H}}B\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)\wedge \left(\neg x\subseteq A{\vee }_{\mathscr{H}}B\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)\right)\leftrightarrow \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B$$
33	31 32	bitrdi	$$⊢x\in \mathrm{HAtoms}\to \left(\left(x\subseteq A{\vee }_{\mathscr{H}}B\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)\leftrightarrow \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)$$
34	33	ralbiia	$$⊢\forall x\in \mathrm{HAtoms}\left(x\subseteq A{\vee }_{\mathscr{H}}B\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)\leftrightarrow \forall x\in \mathrm{HAtoms}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B$$
35	1 2	sumdmdlem2	$$⊢\forall x\in \mathrm{HAtoms}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\to A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B$$
36	34 35	sylbi	$$⊢\forall x\in \mathrm{HAtoms}\left(x\subseteq A{\vee }_{\mathscr{H}}B\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)\to A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B$$
37	1 2	sumdmdi	$$⊢A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B\leftrightarrow A{𝑀}_{\mathscr{H}}^{*}B$$
38	36 37	sylib	$$⊢\forall x\in \mathrm{HAtoms}\left(x\subseteq A{\vee }_{\mathscr{H}}B\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)\to A{𝑀}_{\mathscr{H}}^{*}B$$
39	8 38	impbii	$$⊢A{𝑀}_{\mathscr{H}}^{*}B\leftrightarrow \forall x\in \mathrm{HAtoms}\left(x\subseteq A{\vee }_{\mathscr{H}}B\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)$$
40	2 1	chub2i	$$⊢B\subseteq A{\vee }_{\mathscr{H}}B$$
41	40	biantru	$$⊢x\subseteq A{\vee }_{\mathscr{H}}B\leftrightarrow \left(x\subseteq A{\vee }_{\mathscr{H}}B\wedge B\subseteq A{\vee }_{\mathscr{H}}B\right)$$
42	1 2	chjcli	$$⊢A{\vee }_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}$$
43		chlub	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge A{\vee }_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(x\subseteq A{\vee }_{\mathscr{H}}B\wedge B\subseteq A{\vee }_{\mathscr{H}}B\right)\leftrightarrow x{\vee }_{\mathscr{H}}B\subseteq A{\vee }_{\mathscr{H}}B\right)$$
44	2 42 43	mp3an23	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\left(x\subseteq A{\vee }_{\mathscr{H}}B\wedge B\subseteq A{\vee }_{\mathscr{H}}B\right)\leftrightarrow x{\vee }_{\mathscr{H}}B\subseteq A{\vee }_{\mathscr{H}}B\right)$$
45	41 44	syl5bb	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(x\subseteq A{\vee }_{\mathscr{H}}B\leftrightarrow x{\vee }_{\mathscr{H}}B\subseteq A{\vee }_{\mathscr{H}}B\right)$$
46		ssid	$$⊢x{\vee }_{\mathscr{H}}B\subseteq x{\vee }_{\mathscr{H}}B$$
47	46	biantrur	$$⊢x{\vee }_{\mathscr{H}}B\subseteq A{\vee }_{\mathscr{H}}B\leftrightarrow \left(x{\vee }_{\mathscr{H}}B\subseteq x{\vee }_{\mathscr{H}}B\wedge x{\vee }_{\mathscr{H}}B\subseteq A{\vee }_{\mathscr{H}}B\right)$$
48		ssin	$$⊢\left(x{\vee }_{\mathscr{H}}B\subseteq x{\vee }_{\mathscr{H}}B\wedge x{\vee }_{\mathscr{H}}B\subseteq A{\vee }_{\mathscr{H}}B\right)\leftrightarrow x{\vee }_{\mathscr{H}}B\subseteq \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)$$
49	47 48	bitri	$$⊢x{\vee }_{\mathscr{H}}B\subseteq A{\vee }_{\mathscr{H}}B\leftrightarrow x{\vee }_{\mathscr{H}}B\subseteq \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)$$
50	45 49	bitrdi	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(x\subseteq A{\vee }_{\mathscr{H}}B\leftrightarrow x{\vee }_{\mathscr{H}}B\subseteq \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)$$
51	50	biimpa	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge x\subseteq A{\vee }_{\mathscr{H}}B\right)\to x{\vee }_{\mathscr{H}}B\subseteq \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)$$
52		inss1	$$⊢\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq x{\vee }_{\mathscr{H}}B$$
53	51 52	jctil	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge x\subseteq A{\vee }_{\mathscr{H}}B\right)\to \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq x{\vee }_{\mathscr{H}}B\wedge x{\vee }_{\mathscr{H}}B\subseteq \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)$$
54		eqss	$$⊢\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)=x{\vee }_{\mathscr{H}}B\leftrightarrow \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq x{\vee }_{\mathscr{H}}B\wedge x{\vee }_{\mathscr{H}}B\subseteq \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)$$
55	53 54	sylibr	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge x\subseteq A{\vee }_{\mathscr{H}}B\right)\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)=x{\vee }_{\mathscr{H}}B$$
56	55	sseq1d	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge x\subseteq A{\vee }_{\mathscr{H}}B\right)\to \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\leftrightarrow x{\vee }_{\mathscr{H}}B\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)$$
57	2 22	mpan2	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to x{\vee }_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}$$
58	57 1 24	sylancl	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(x{\vee }_{\mathscr{H}}B\right)\cap A\in {\mathbf{C}}_{\mathscr{H}}$$
59	2 58 26	sylancr	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to B\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B$$
60	59	biantrud	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(x\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\leftrightarrow \left(x\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\wedge B\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)\right)$$
61		chjcl	$$⊢\left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}$$
62	58 2 61	sylancl	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}$$
63		chlub	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(x\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\wedge B\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)\leftrightarrow x{\vee }_{\mathscr{H}}B\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)$$
64	2 63	mp3an2	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(x\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\wedge B\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)\leftrightarrow x{\vee }_{\mathscr{H}}B\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)$$
65	62 64	mpdan	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\left(x\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\wedge B\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)\leftrightarrow x{\vee }_{\mathscr{H}}B\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)$$
66	60 65	bitrd	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(x\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\leftrightarrow x{\vee }_{\mathscr{H}}B\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)$$
67	66	adantr	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge x\subseteq A{\vee }_{\mathscr{H}}B\right)\to \left(x\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\leftrightarrow x{\vee }_{\mathscr{H}}B\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)$$
68	56 67	bitr4d	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge x\subseteq A{\vee }_{\mathscr{H}}B\right)\to \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\leftrightarrow x\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)$$
69	68	pm5.74da	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\left(x\subseteq A{\vee }_{\mathscr{H}}B\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)\leftrightarrow \left(x\subseteq A{\vee }_{\mathscr{H}}B\to x\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)\right)$$
70	5 69	syl	$$⊢x\in \mathrm{HAtoms}\to \left(\left(x\subseteq A{\vee }_{\mathscr{H}}B\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)\leftrightarrow \left(x\subseteq A{\vee }_{\mathscr{H}}B\to x\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)\right)$$
71	70	ralbiia	$$⊢\forall x\in \mathrm{HAtoms}\left(x\subseteq A{\vee }_{\mathscr{H}}B\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)\leftrightarrow \forall x\in \mathrm{HAtoms}\left(x\subseteq A{\vee }_{\mathscr{H}}B\to x\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)$$
72	39 71	bitri	$$⊢A{𝑀}_{\mathscr{H}}^{*}B\leftrightarrow \forall x\in \mathrm{HAtoms}\left(x\subseteq A{\vee }_{\mathscr{H}}B\to x\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)$$