Theorem chrelat4i

Description: A consequence of relative atomicity. Extensionality principle: two lattice elements are equal iff they majorize the same atoms. (Contributed by NM, 30-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	chrelat3.1	|- A e. CH
	chrelat3.2	|- B e. CH
Assertion	chrelat4i	|- ( A = B <-> A. x e. HAtoms ( x C_ A <-> x C_ B ) )

Proof

Step	Hyp	Ref	Expression
1		chrelat3.1	|- A e. CH
2		chrelat3.2	|- B e. CH
3	1 2	chrelat3i	|- ( A C_ B <-> A. x e. HAtoms ( x C_ A -> x C_ B ) )
4	2 1	chrelat3i	|- ( B C_ A <-> A. x e. HAtoms ( x C_ B -> x C_ A ) )
5	3 4	anbi12i	|- ( ( A C_ B /\ B C_ A ) <-> ( A. x e. HAtoms ( x C_ A -> x C_ B ) /\ A. x e. HAtoms ( x C_ B -> x C_ A ) ) )
6		eqss	|- ( A = B <-> ( A C_ B /\ B C_ A ) )
7		ralbiim	|- ( A. x e. HAtoms ( x C_ A <-> x C_ B ) <-> ( A. x e. HAtoms ( x C_ A -> x C_ B ) /\ A. x e. HAtoms ( x C_ B -> x C_ A ) ) )
8	5 6 7	3bitr4i	|- ( A = B <-> A. x e. HAtoms ( x C_ A <-> x C_ B ) )