Metamath Proof Explorer


Theorem lecmi

Description: Comparable Hilbert lattice elements commute. Theorem 2.3(iii) of Beran p. 40. (Contributed by NM, 16-Jan-2005) (New usage is discouraged.)

Ref Expression
Hypotheses pjoml2.1 𝐴C
pjoml2.2 𝐵C
Assertion lecmi ( 𝐴𝐵𝐴 𝐶 𝐵 )

Proof

Step Hyp Ref Expression
1 pjoml2.1 𝐴C
2 pjoml2.2 𝐵C
3 ssinss1 ( 𝐴𝐵 → ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ 𝐵 ) ) ⊆ 𝐵 )
4 1 2 cmbr4i ( 𝐴 𝐶 𝐵 ↔ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ 𝐵 ) ) ⊆ 𝐵 )
5 3 4 sylibr ( 𝐴𝐵𝐴 𝐶 𝐵 )