Metamath Proof Explorer


Theorem meetat2

Description: The meet of any element with an atom is either the atom or zero. (Contributed by NM, 30-Aug-2012)

Ref Expression
Hypotheses m.b 𝐵 = ( Base ‘ 𝐾 )
m.m = ( meet ‘ 𝐾 )
m.z 0 = ( 0. ‘ 𝐾 )
m.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion meetat2 ( ( 𝐾 ∈ OL ∧ 𝑋𝐵𝑃𝐴 ) → ( ( 𝑋 𝑃 ) ∈ 𝐴 ∨ ( 𝑋 𝑃 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 m.b 𝐵 = ( Base ‘ 𝐾 )
2 m.m = ( meet ‘ 𝐾 )
3 m.z 0 = ( 0. ‘ 𝐾 )
4 m.a 𝐴 = ( Atoms ‘ 𝐾 )
5 1 2 3 4 meetat ( ( 𝐾 ∈ OL ∧ 𝑋𝐵𝑃𝐴 ) → ( ( 𝑋 𝑃 ) = 𝑃 ∨ ( 𝑋 𝑃 ) = 0 ) )
6 eleq1a ( 𝑃𝐴 → ( ( 𝑋 𝑃 ) = 𝑃 → ( 𝑋 𝑃 ) ∈ 𝐴 ) )
7 6 3ad2ant3 ( ( 𝐾 ∈ OL ∧ 𝑋𝐵𝑃𝐴 ) → ( ( 𝑋 𝑃 ) = 𝑃 → ( 𝑋 𝑃 ) ∈ 𝐴 ) )
8 7 orim1d ( ( 𝐾 ∈ OL ∧ 𝑋𝐵𝑃𝐴 ) → ( ( ( 𝑋 𝑃 ) = 𝑃 ∨ ( 𝑋 𝑃 ) = 0 ) → ( ( 𝑋 𝑃 ) ∈ 𝐴 ∨ ( 𝑋 𝑃 ) = 0 ) ) )
9 5 8 mpd ( ( 𝐾 ∈ OL ∧ 𝑋𝐵𝑃𝐴 ) → ( ( 𝑋 𝑃 ) ∈ 𝐴 ∨ ( 𝑋 𝑃 ) = 0 ) )