Metamath Proof Explorer

Theorem ssdmd1

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

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

Proof

Step	Hyp	Ref	Expression
1		choccl	$⊢ B \in C_{ℋ} \to ⊥ (B) \in C_{ℋ}$
2		choccl	$⊢ A \in C_{ℋ} \to ⊥ (A) \in C_{ℋ}$
3		ssmd2	$⊢ (⊥ (B) \in C_{ℋ} \land ⊥ (A) \in C_{ℋ} \land ⊥ (B) \subseteq ⊥ (A)) \to ⊥ (A) 𝑀_{ℋ} ⊥ (B)$
4	3	3expia	$⊢ (⊥ (B) \in C_{ℋ} \land ⊥ (A) \in C_{ℋ}) \to (⊥ (B) \subseteq ⊥ (A) \to ⊥ (A) 𝑀_{ℋ} ⊥ (B))$
5	1 2 4	syl2anr	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (⊥ (B) \subseteq ⊥ (A) \to ⊥ (A) 𝑀_{ℋ} ⊥ (B))$
6		chsscon3	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A \subseteq B \leftrightarrow ⊥ (B) \subseteq ⊥ (A))$
7		dmdmd	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A 𝑀_{ℋ}^{*} B \leftrightarrow ⊥ (A) 𝑀_{ℋ} ⊥ (B))$
8	5 6 7	3imtr4d	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A \subseteq B \to A 𝑀_{ℋ}^{*} B)$
9	8	3impia	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land A \subseteq B) \to A 𝑀_{ℋ}^{*} B$