ssmd1

Description: Ordering implies the modular pair property. Remark in MaedaMaeda p. 1. (Contributed by NM, 21-Jun-2004) (New usage is discouraged.)

		Ref	Expression
	Assertion	ssmd1	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land A \subseteq B) \to A 𝑀_{ℋ} B$

Step	Hyp	Ref	Expression
1		inss1	$⊢ (x \lor_{ℋ} A) \cap B \subseteq x \lor_{ℋ} A$
2		dfss	$⊢ A \subseteq B \leftrightarrow A = A \cap B$
3	2	biimpi	$⊢ A \subseteq B \to A = A \cap B$
4	3	oveq2d	$⊢ A \subseteq B \to x \lor_{ℋ} A = x \lor_{ℋ} (A \cap B)$
5	1 4	sseqtrid	$⊢ A \subseteq B \to (x \lor_{ℋ} A) \cap B \subseteq x \lor_{ℋ} (A \cap B)$
6	5	a1d	$⊢ A \subseteq B \to (x \subseteq B \to (x \lor_{ℋ} A) \cap B \subseteq x \lor_{ℋ} (A \cap B))$
7	6	ralrimivw	$⊢ A \subseteq B \to \forall x \in C_{ℋ} (x \subseteq B \to (x \lor_{ℋ} A) \cap B \subseteq x \lor_{ℋ} (A \cap B))$
8		mdbr2	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A 𝑀_{ℋ} B \leftrightarrow \forall x \in C_{ℋ} (x \subseteq B \to (x \lor_{ℋ} A) \cap B \subseteq x \lor_{ℋ} (A \cap B)))$
9	7 8	imbitrrid	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A \subseteq B \to A 𝑀_{ℋ} B)$
10	9	3impia	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land A \subseteq B) \to A 𝑀_{ℋ} B$

Metamath Proof Explorer