Metamath Proof Explorer

Theorem dmdbr4ati

Description: Dual modular pair property in terms of atoms. (Contributed by NM, 15-Jan-2005) (New usage is discouraged.)

Ref Expression
Hypotheses sumdmdi.1 ⊢ A ∈ C ℋ
sumdmdi.2 ⊢ B ∈ C ℋ
Assertion dmdbr4ati ⊢ A 𝑀 ℋ * B ↔ ∀ x ∈ HAtoms x ∨ ℋ B ∩ A ∨ ℋ B ⊆ x ∨ ℋ B ∩ A ∨ ℋ B

Proof

Step Hyp Ref Expression
1 sumdmdi.1 ⊢ A ∈ C ℋ
2 sumdmdi.2 ⊢ B ∈ C ℋ
3 dmdbr4 ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A 𝑀 ℋ * B ↔ ∀ x ∈ C ℋ x ∨ ℋ B ∩ A ∨ ℋ B ⊆ x ∨ ℋ B ∩ A ∨ ℋ B
4 1 2 3 mp2an ⊢ A 𝑀 ℋ * B ↔ ∀ x ∈ C ℋ x ∨ ℋ B ∩ A ∨ ℋ B ⊆ x ∨ ℋ B ∩ A ∨ ℋ B
5 atelch ⊢ x ∈ HAtoms → x ∈ C ℋ
6 5 imim1i ⊢ x ∈ C ℋ → x ∨ ℋ B ∩ A ∨ ℋ B ⊆ x ∨ ℋ B ∩ A ∨ ℋ B → x ∈ HAtoms → x ∨ ℋ B ∩ A ∨ ℋ B ⊆ x ∨ ℋ B ∩ A ∨ ℋ B
7 6 ralimi2 ⊢ ∀ x ∈ C ℋ x ∨ ℋ B ∩ A ∨ ℋ B ⊆ x ∨ ℋ B ∩ A ∨ ℋ B → ∀ x ∈ HAtoms x ∨ ℋ B ∩ A ∨ ℋ B ⊆ x ∨ ℋ B ∩ A ∨ ℋ B
8 4 7 sylbi ⊢ A 𝑀 ℋ * B → ∀ x ∈ HAtoms x ∨ ℋ B ∩ A ∨ ℋ B ⊆ x ∨ ℋ B ∩ A ∨ ℋ B
9 1 2 sumdmdlem2 ⊢ ∀ x ∈ HAtoms x ∨ ℋ B ∩ A ∨ ℋ B ⊆ x ∨ ℋ B ∩ A ∨ ℋ B → A + ℋ B = A ∨ ℋ B
10 1 2 sumdmdi ⊢ A + ℋ B = A ∨ ℋ B ↔ A 𝑀 ℋ * B
11 9 10 sylib ⊢ ∀ x ∈ HAtoms x ∨ ℋ B ∩ A ∨ ℋ B ⊆ x ∨ ℋ B ∩ A ∨ ℋ B → A 𝑀 ℋ * B
12 8 11 impbii ⊢ A 𝑀 ℋ * B ↔ ∀ x ∈ HAtoms x ∨ ℋ B ∩ A ∨ ℋ B ⊆ x ∨ ℋ B ∩ A ∨ ℋ B