Metamath Proof Explorer


Theorem atssma

Description: The meet with an atom's superset is the atom. (Contributed by NM, 12-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion atssma ( ( 𝐴 ∈ HAtoms ∧ 𝐵C ) → ( 𝐴𝐵 ↔ ( 𝐴𝐵 ) ∈ HAtoms ) )

Proof

Step Hyp Ref Expression
1 df-ss ( 𝐴𝐵 ↔ ( 𝐴𝐵 ) = 𝐴 )
2 1 biimpi ( 𝐴𝐵 → ( 𝐴𝐵 ) = 𝐴 )
3 2 eleq1d ( 𝐴𝐵 → ( ( 𝐴𝐵 ) ∈ HAtoms ↔ 𝐴 ∈ HAtoms ) )
4 3 biimprcd ( 𝐴 ∈ HAtoms → ( 𝐴𝐵 → ( 𝐴𝐵 ) ∈ HAtoms ) )
5 4 adantr ( ( 𝐴 ∈ HAtoms ∧ 𝐵C ) → ( 𝐴𝐵 → ( 𝐴𝐵 ) ∈ HAtoms ) )
6 incom ( 𝐴𝐵 ) = ( 𝐵𝐴 )
7 6 eleq1i ( ( 𝐴𝐵 ) ∈ HAtoms ↔ ( 𝐵𝐴 ) ∈ HAtoms )
8 atne0 ( ( 𝐵𝐴 ) ∈ HAtoms → ( 𝐵𝐴 ) ≠ 0 )
9 8 neneqd ( ( 𝐵𝐴 ) ∈ HAtoms → ¬ ( 𝐵𝐴 ) = 0 )
10 7 9 sylbi ( ( 𝐴𝐵 ) ∈ HAtoms → ¬ ( 𝐵𝐴 ) = 0 )
11 atnssm0 ( ( 𝐵C𝐴 ∈ HAtoms ) → ( ¬ 𝐴𝐵 ↔ ( 𝐵𝐴 ) = 0 ) )
12 11 ancoms ( ( 𝐴 ∈ HAtoms ∧ 𝐵C ) → ( ¬ 𝐴𝐵 ↔ ( 𝐵𝐴 ) = 0 ) )
13 12 biimpd ( ( 𝐴 ∈ HAtoms ∧ 𝐵C ) → ( ¬ 𝐴𝐵 → ( 𝐵𝐴 ) = 0 ) )
14 13 con1d ( ( 𝐴 ∈ HAtoms ∧ 𝐵C ) → ( ¬ ( 𝐵𝐴 ) = 0𝐴𝐵 ) )
15 10 14 syl5 ( ( 𝐴 ∈ HAtoms ∧ 𝐵C ) → ( ( 𝐴𝐵 ) ∈ HAtoms → 𝐴𝐵 ) )
16 5 15 impbid ( ( 𝐴 ∈ HAtoms ∧ 𝐵C ) → ( 𝐴𝐵 ↔ ( 𝐴𝐵 ) ∈ HAtoms ) )