Metamath Proof Explorer

Theorem mddmd

Description: The modular pair property expressed in terms of the dual modular pair property. (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		choccl	$⊢ A \in C_{ℋ} \to ⊥ (A) \in C_{ℋ}$
2		choccl	$⊢ B \in C_{ℋ} \to ⊥ (B) \in C_{ℋ}$
3		dmdmd	$⊢ (⊥ (A) \in C_{ℋ} \land ⊥ (B) \in C_{ℋ}) \to (⊥ (A) 𝑀_{ℋ}^{*} ⊥ (B) \leftrightarrow ⊥ (⊥ (A)) 𝑀_{ℋ} ⊥ (⊥ (B)))$
4	1 2 3	syl2an	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (⊥ (A) 𝑀_{ℋ}^{*} ⊥ (B) \leftrightarrow ⊥ (⊥ (A)) 𝑀_{ℋ} ⊥ (⊥ (B)))$
5		ococ	$⊢ A \in C_{ℋ} \to ⊥ (⊥ (A)) = A$
6		ococ	$⊢ B \in C_{ℋ} \to ⊥ (⊥ (B)) = B$
7	5 6	breqan12d	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (⊥ (⊥ (A)) 𝑀_{ℋ} ⊥ (⊥ (B)) \leftrightarrow A 𝑀_{ℋ} B)$
8	4 7	bitr2d	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A 𝑀_{ℋ} B \leftrightarrow ⊥ (A) 𝑀_{ℋ}^{*} ⊥ (B))$