Theorem dmdi2

Description: Consequence of the dual modular pair property. (Contributed by NM, 14-Jan-2005) (New usage is discouraged.)

	Ref	Expression
Assertion	dmdi2	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \left(A{𝑀}_{\mathscr{H}}^{*}B\wedge B\subseteq C\right)\right)\to C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(C\cap A\right){\vee }_{\mathscr{H}}B$$

Proof

Step	Hyp	Ref	Expression
1		dmdi	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \left(A{𝑀}_{\mathscr{H}}^{*}B\wedge B\subseteq C\right)\right)\to \left(C\cap A\right){\vee }_{\mathscr{H}}B=C\cap \left(A{\vee }_{\mathscr{H}}B\right)$$
2		eqimss2	$$⊢\left(C\cap A\right){\vee }_{\mathscr{H}}B=C\cap \left(A{\vee }_{\mathscr{H}}B\right)\to C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(C\cap A\right){\vee }_{\mathscr{H}}B$$
3	1 2	syl	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \left(A{𝑀}_{\mathscr{H}}^{*}B\wedge B\subseteq C\right)\right)\to C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(C\cap A\right){\vee }_{\mathscr{H}}B$$