Metamath Proof Explorer


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 AC
chrelat3.2 BC
Assertion chrelat4i A=BxHAtomsxAxB

Proof

Step Hyp Ref Expression
1 chrelat3.1 AC
2 chrelat3.2 BC
3 1 2 chrelat3i ABxHAtomsxAxB
4 2 1 chrelat3i BAxHAtomsxBxA
5 3 4 anbi12i ABBAxHAtomsxAxBxHAtomsxBxA
6 eqss A=BABBA
7 ralbiim xHAtomsxAxBxHAtomsxAxBxHAtomsxBxA
8 5 6 7 3bitr4i A=BxHAtomsxAxB