Metamath Proof Explorer

Theorem ssdmd2

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	ssdmd2	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land A \subseteq B) \to ⊥ (B) 𝑀_{ℋ} ⊥ (A)$

Proof

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