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 𝐴C
chrelat3.2 𝐵C
Assertion chrelat4i ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ∈ HAtoms ( 𝑥𝐴𝑥𝐵 ) )

Proof

Step Hyp Ref Expression
1 chrelat3.1 𝐴C
2 chrelat3.2 𝐵C
3 1 2 chrelat3i ( 𝐴𝐵 ↔ ∀ 𝑥 ∈ HAtoms ( 𝑥𝐴𝑥𝐵 ) )
4 2 1 chrelat3i ( 𝐵𝐴 ↔ ∀ 𝑥 ∈ HAtoms ( 𝑥𝐵𝑥𝐴 ) )
5 3 4 anbi12i ( ( 𝐴𝐵𝐵𝐴 ) ↔ ( ∀ 𝑥 ∈ HAtoms ( 𝑥𝐴𝑥𝐵 ) ∧ ∀ 𝑥 ∈ HAtoms ( 𝑥𝐵𝑥𝐴 ) ) )
6 eqss ( 𝐴 = 𝐵 ↔ ( 𝐴𝐵𝐵𝐴 ) )
7 ralbiim ( ∀ 𝑥 ∈ HAtoms ( 𝑥𝐴𝑥𝐵 ) ↔ ( ∀ 𝑥 ∈ HAtoms ( 𝑥𝐴𝑥𝐵 ) ∧ ∀ 𝑥 ∈ HAtoms ( 𝑥𝐵𝑥𝐴 ) ) )
8 5 6 7 3bitr4i ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ∈ HAtoms ( 𝑥𝐴𝑥𝐵 ) )