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 e. CH
	sumdmdi.2	|- B e. CH
Assertion	dmdbr4ati	|- ( A MH* B <-> A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) )

Proof

Step	Hyp	Ref	Expression
1		sumdmdi.1	|- A e. CH
2		sumdmdi.2	|- B e. CH
3		dmdbr4	|- ( ( A e. CH /\ B e. CH ) -> ( A MH* B <-> A. x e. CH ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) ) )
4	1 2 3	mp2an	|- ( A MH* B <-> A. x e. CH ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) )
5		atelch	|- ( x e. HAtoms -> x e. CH )
6	5	imim1i	|- ( ( x e. CH -> ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) ) -> ( x e. HAtoms -> ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) ) )
7	6	ralimi2	|- ( A. x e. CH ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) -> A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) )
8	4 7	sylbi	|- ( A MH* B -> A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) )
9	1 2	sumdmdlem2	|- ( A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) -> ( A +H B ) = ( A vH B ) )
10	1 2	sumdmdi	|- ( ( A +H B ) = ( A vH B ) <-> A MH* B )
11	9 10	sylib	|- ( A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) -> A MH* B )
12	8 11	impbii	|- ( A MH* B <-> A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) )