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

Proof

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