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	⊢ 𝐴 ∈ Cℋ
	sumdmdi.2	⊢ 𝐵 ∈ Cℋ
Assertion	dmdbr4ati	⊢ ( 𝐴 𝑀ℋ* 𝐵 ↔ ∀ 𝑥 ∈ HAtoms ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) )

Proof

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