Metamath Proof Explorer

Theorem dmdbr7ati

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

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

Proof

Step Hyp Ref Expression
1 sumdmdi.1 ⊢ A ∈ C ℋ
2 sumdmdi.2 ⊢ B ∈ C ℋ
3 1 2 dmdbr6ati ⊢ A 𝑀 ℋ * B ↔ ∀ x ∈ HAtoms A ∨ ℋ B ∩ x = x ∨ ℋ B ∩ A ∨ ℋ B ∩ x
4 inss1 ⊢ x ∨ ℋ B ∩ A ∨ ℋ B ∩ x ⊆ x ∨ ℋ B ∩ A ∨ ℋ B
5 sseq1 ⊢ A ∨ ℋ B ∩ x = x ∨ ℋ B ∩ A ∨ ℋ B ∩ x → A ∨ ℋ B ∩ x ⊆ x ∨ ℋ B ∩ A ∨ ℋ B ↔ x ∨ ℋ B ∩ A ∨ ℋ B ∩ x ⊆ x ∨ ℋ B ∩ A ∨ ℋ B
6 4 5 mpbiri ⊢ A ∨ ℋ B ∩ x = x ∨ ℋ B ∩ A ∨ ℋ B ∩ x → A ∨ ℋ B ∩ x ⊆ x ∨ ℋ B ∩ A ∨ ℋ B
7 6 ralimi ⊢ ∀ x ∈ HAtoms A ∨ ℋ B ∩ x = x ∨ ℋ B ∩ A ∨ ℋ B ∩ x → ∀ x ∈ HAtoms A ∨ ℋ B ∩ x ⊆ x ∨ ℋ B ∩ A ∨ ℋ B
8 3 7 sylbi ⊢ A 𝑀 ℋ * B → ∀ x ∈ HAtoms A ∨ ℋ B ∩ x ⊆ x ∨ ℋ B ∩ A ∨ ℋ B
9 sseqin2 ⊢ x ⊆ A ∨ ℋ B ↔ A ∨ ℋ B ∩ x = x
10 9 biimpi ⊢ x ⊆ A ∨ ℋ B → A ∨ ℋ B ∩ x = x
11 10 sseq1d ⊢ x ⊆ A ∨ ℋ B → A ∨ ℋ B ∩ x ⊆ x ∨ ℋ B ∩ A ∨ ℋ B ↔ x ⊆ x ∨ ℋ B ∩ A ∨ ℋ B
12 11 biimpcd ⊢ A ∨ ℋ B ∩ x ⊆ x ∨ ℋ B ∩ A ∨ ℋ B → x ⊆ A ∨ ℋ B → x ⊆ x ∨ ℋ B ∩ A ∨ ℋ B
13 12 ralimi ⊢ ∀ x ∈ HAtoms A ∨ ℋ B ∩ x ⊆ x ∨ ℋ B ∩ A ∨ ℋ B → ∀ x ∈ HAtoms x ⊆ A ∨ ℋ B → x ⊆ x ∨ ℋ B ∩ A ∨ ℋ B
14 1 2 dmdbr5ati ⊢ A 𝑀 ℋ * B ↔ ∀ x ∈ HAtoms x ⊆ A ∨ ℋ B → x ⊆ x ∨ ℋ B ∩ A ∨ ℋ B
15 13 14 sylibr ⊢ ∀ x ∈ HAtoms A ∨ ℋ B ∩ x ⊆ x ∨ ℋ B ∩ A ∨ ℋ B → A 𝑀 ℋ * B
16 8 15 impbii ⊢ A 𝑀 ℋ * B ↔ ∀ x ∈ HAtoms A ∨ ℋ B ∩ x ⊆ x ∨ ℋ B ∩ A ∨ ℋ B