Metamath Proof Explorer


Theorem chrelat3i

Description: A consequence of the relative atomicity of Hilbert space: the ordering of Hilbert lattice elements is completely determined by the atoms they majorize. (Contributed by NM, 30-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypotheses chrelat3.1 𝐴C
chrelat3.2 𝐵C
Assertion chrelat3i ( 𝐴𝐵 ↔ ∀ 𝑥 ∈ HAtoms ( 𝑥𝐴𝑥𝐵 ) )

Proof

Step Hyp Ref Expression
1 chrelat3.1 𝐴C
2 chrelat3.2 𝐵C
3 chrelat3 ( ( 𝐴C𝐵C ) → ( 𝐴𝐵 ↔ ∀ 𝑥 ∈ HAtoms ( 𝑥𝐴𝑥𝐵 ) ) )
4 1 2 3 mp2an ( 𝐴𝐵 ↔ ∀ 𝑥 ∈ HAtoms ( 𝑥𝐴𝑥𝐵 ) )