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 ∈ C ℋ ∧ B ∈ C ℋ → A 𝑀 ℋ B ↔ ⊥ ⁡ A 𝑀 ℋ * ⊥ ⁡ B

Proof

Step Hyp Ref Expression
1 choccl ⊢ A ∈ C ℋ → ⊥ ⁡ A ∈ C ℋ
2 choccl ⊢ B ∈ C ℋ → ⊥ ⁡ B ∈ C ℋ
3 dmdmd ⊢ ⊥ ⁡ A ∈ C ℋ ∧ ⊥ ⁡ B ∈ C ℋ → ⊥ ⁡ A 𝑀 ℋ * ⊥ ⁡ B ↔ ⊥ ⁡ ⊥ ⁡ A 𝑀 ℋ ⊥ ⁡ ⊥ ⁡ B
4 1 2 3 syl2an ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → ⊥ ⁡ A 𝑀 ℋ * ⊥ ⁡ B ↔ ⊥ ⁡ ⊥ ⁡ A 𝑀 ℋ ⊥ ⁡ ⊥ ⁡ B
5 ococ ⊢ A ∈ C ℋ → ⊥ ⁡ ⊥ ⁡ A = A
6 ococ ⊢ B ∈ C ℋ → ⊥ ⁡ ⊥ ⁡ B = B
7 5 6 breqan12d ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → ⊥ ⁡ ⊥ ⁡ A 𝑀 ℋ ⊥ ⁡ ⊥ ⁡ B ↔ A 𝑀 ℋ B
8 4 7 bitr2d ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A 𝑀 ℋ B ↔ ⊥ ⁡ A 𝑀 ℋ * ⊥ ⁡ B