Theorem mdsymlem1

Description: Lemma for mdsymi . (Contributed by NM, 1-Jul-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mdsymlem1.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	mdsymlem1.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
	mdsymlem1.3	$$⊢C=A{\vee }_{\mathscr{H}}p$$
Assertion	mdsymlem1	$$⊢\left(\left(p\in {\mathbf{C}}_{\mathscr{H}}\wedge B\cap C\subseteq A\right)\wedge \left(B{𝑀}_{\mathscr{H}}^{*}A\wedge p\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\to p\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		mdsymlem1.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		mdsymlem1.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3		mdsymlem1.3	$$⊢C=A{\vee }_{\mathscr{H}}p$$
4		chub2	$$⊢\left(p\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\right)\to p\subseteq A{\vee }_{\mathscr{H}}p$$
5	1 4	mpan2	$$⊢p\in {\mathbf{C}}_{\mathscr{H}}\to p\subseteq A{\vee }_{\mathscr{H}}p$$
6	5 3	sseqtrrdi	$$⊢p\in {\mathbf{C}}_{\mathscr{H}}\to p\subseteq C$$
7	1 2	chjcomi	$$⊢A{\vee }_{\mathscr{H}}B=B{\vee }_{\mathscr{H}}A$$
8	7	sseq2i	$$⊢p\subseteq A{\vee }_{\mathscr{H}}B\leftrightarrow p\subseteq B{\vee }_{\mathscr{H}}A$$
9	8	biimpi	$$⊢p\subseteq A{\vee }_{\mathscr{H}}B\to p\subseteq B{\vee }_{\mathscr{H}}A$$
10	6 9	anim12i	$$⊢\left(p\in {\mathbf{C}}_{\mathscr{H}}\wedge p\subseteq A{\vee }_{\mathscr{H}}B\right)\to \left(p\subseteq C\wedge p\subseteq B{\vee }_{\mathscr{H}}A\right)$$
11		ssin	$$⊢\left(p\subseteq C\wedge p\subseteq B{\vee }_{\mathscr{H}}A\right)\leftrightarrow p\subseteq C\cap \left(B{\vee }_{\mathscr{H}}A\right)$$
12	10 11	sylib	$$⊢\left(p\in {\mathbf{C}}_{\mathscr{H}}\wedge p\subseteq A{\vee }_{\mathscr{H}}B\right)\to p\subseteq C\cap \left(B{\vee }_{\mathscr{H}}A\right)$$
13	12	ad2ant2rl	$$⊢\left(\left(p\in {\mathbf{C}}_{\mathscr{H}}\wedge B\cap C\subseteq A\right)\wedge \left(B{𝑀}_{\mathscr{H}}^{*}A\wedge p\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\to p\subseteq C\cap \left(B{\vee }_{\mathscr{H}}A\right)$$
14		chjcl	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge p\in {\mathbf{C}}_{\mathscr{H}}\right)\to A{\vee }_{\mathscr{H}}p\in {\mathbf{C}}_{\mathscr{H}}$$
15	1 14	mpan	$$⊢p\in {\mathbf{C}}_{\mathscr{H}}\to A{\vee }_{\mathscr{H}}p\in {\mathbf{C}}_{\mathscr{H}}$$
16	3 15	eqeltrid	$$⊢p\in {\mathbf{C}}_{\mathscr{H}}\to C\in {\mathbf{C}}_{\mathscr{H}}$$
17	16	adantr	$$⊢\left(p\in {\mathbf{C}}_{\mathscr{H}}\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\to C\in {\mathbf{C}}_{\mathscr{H}}$$
18		chub1	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge p\in {\mathbf{C}}_{\mathscr{H}}\right)\to A\subseteq A{\vee }_{\mathscr{H}}p$$
19	1 18	mpan	$$⊢p\in {\mathbf{C}}_{\mathscr{H}}\to A\subseteq A{\vee }_{\mathscr{H}}p$$
20	19 3	sseqtrrdi	$$⊢p\in {\mathbf{C}}_{\mathscr{H}}\to A\subseteq C$$
21	20	anim2i	$$⊢\left(B{𝑀}_{\mathscr{H}}^{*}A\wedge p\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(B{𝑀}_{\mathscr{H}}^{*}A\wedge A\subseteq C\right)$$
22	21	ancoms	$$⊢\left(p\in {\mathbf{C}}_{\mathscr{H}}\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\to \left(B{𝑀}_{\mathscr{H}}^{*}A\wedge A\subseteq C\right)$$
23		dmdi	$$⊢\left(\left(B\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \left(B{𝑀}_{\mathscr{H}}^{*}A\wedge A\subseteq C\right)\right)\to \left(C\cap B\right){\vee }_{\mathscr{H}}A=C\cap \left(B{\vee }_{\mathscr{H}}A\right)$$
24	2 23	mp3anl1	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \left(B{𝑀}_{\mathscr{H}}^{*}A\wedge A\subseteq C\right)\right)\to \left(C\cap B\right){\vee }_{\mathscr{H}}A=C\cap \left(B{\vee }_{\mathscr{H}}A\right)$$
25	1 24	mpanl1	$$⊢\left(C\in {\mathbf{C}}_{\mathscr{H}}\wedge \left(B{𝑀}_{\mathscr{H}}^{*}A\wedge A\subseteq C\right)\right)\to \left(C\cap B\right){\vee }_{\mathscr{H}}A=C\cap \left(B{\vee }_{\mathscr{H}}A\right)$$
26	17 22 25	syl2anc	$$⊢\left(p\in {\mathbf{C}}_{\mathscr{H}}\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\to \left(C\cap B\right){\vee }_{\mathscr{H}}A=C\cap \left(B{\vee }_{\mathscr{H}}A\right)$$
27	26	adantlr	$$⊢\left(\left(p\in {\mathbf{C}}_{\mathscr{H}}\wedge B\cap C\subseteq A\right)\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\to \left(C\cap B\right){\vee }_{\mathscr{H}}A=C\cap \left(B{\vee }_{\mathscr{H}}A\right)$$
28		incom	$$⊢C\cap B=B\cap C$$
29	28	oveq1i	$$⊢\left(C\cap B\right){\vee }_{\mathscr{H}}A=\left(B\cap C\right){\vee }_{\mathscr{H}}A$$
30		chincl	$$⊢\left(B\in {\mathbf{C}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\to B\cap C\in {\mathbf{C}}_{\mathscr{H}}$$
31	2 30	mpan	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}\to B\cap C\in {\mathbf{C}}_{\mathscr{H}}$$
32		chlejb1	$$⊢\left(B\cap C\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(B\cap C\subseteq A\leftrightarrow \left(B\cap C\right){\vee }_{\mathscr{H}}A=A\right)$$
33	1 32	mpan2	$$⊢B\cap C\in {\mathbf{C}}_{\mathscr{H}}\to \left(B\cap C\subseteq A\leftrightarrow \left(B\cap C\right){\vee }_{\mathscr{H}}A=A\right)$$
34	16 31 33	3syl	$$⊢p\in {\mathbf{C}}_{\mathscr{H}}\to \left(B\cap C\subseteq A\leftrightarrow \left(B\cap C\right){\vee }_{\mathscr{H}}A=A\right)$$
35	34	biimpa	$$⊢\left(p\in {\mathbf{C}}_{\mathscr{H}}\wedge B\cap C\subseteq A\right)\to \left(B\cap C\right){\vee }_{\mathscr{H}}A=A$$
36	29 35	syl5eq	$$⊢\left(p\in {\mathbf{C}}_{\mathscr{H}}\wedge B\cap C\subseteq A\right)\to \left(C\cap B\right){\vee }_{\mathscr{H}}A=A$$
37	36	adantr	$$⊢\left(\left(p\in {\mathbf{C}}_{\mathscr{H}}\wedge B\cap C\subseteq A\right)\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\to \left(C\cap B\right){\vee }_{\mathscr{H}}A=A$$
38	27 37	eqtr3d	$$⊢\left(\left(p\in {\mathbf{C}}_{\mathscr{H}}\wedge B\cap C\subseteq A\right)\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\to C\cap \left(B{\vee }_{\mathscr{H}}A\right)=A$$
39	38	adantrr	$$⊢\left(\left(p\in {\mathbf{C}}_{\mathscr{H}}\wedge B\cap C\subseteq A\right)\wedge \left(B{𝑀}_{\mathscr{H}}^{*}A\wedge p\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\to C\cap \left(B{\vee }_{\mathscr{H}}A\right)=A$$
40	13 39	sseqtrd	$$⊢\left(\left(p\in {\mathbf{C}}_{\mathscr{H}}\wedge B\cap C\subseteq A\right)\wedge \left(B{𝑀}_{\mathscr{H}}^{*}A\wedge p\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\to p\subseteq A$$