This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ( A e. HAtoms /\ B e. CH ) -> ( A C_ B <-> ( A i^i B ) e. HAtoms ) )

Proof

Step Hyp Ref Expression
1 dfss2 
 |-  ( A C_ B <-> ( A i^i B ) = A )
2 1 biimpi 
 |-  ( A C_ B -> ( A i^i B ) = A )
3 2 eleq1d 
 |-  ( A C_ B -> ( ( A i^i B ) e. HAtoms <-> A e. HAtoms ) )
4 3 biimprcd 
 |-  ( A e. HAtoms -> ( A C_ B -> ( A i^i B ) e. HAtoms ) )
5 4 adantr 
 |-  ( ( A e. HAtoms /\ B e. CH ) -> ( A C_ B -> ( A i^i B ) e. HAtoms ) )
6 incom 
 |-  ( A i^i B ) = ( B i^i A )
7 6 eleq1i 
 |-  ( ( A i^i B ) e. HAtoms <-> ( B i^i A ) e. HAtoms )
8 atne0 
 |-  ( ( B i^i A ) e. HAtoms -> ( B i^i A ) =/= 0H )
9 8 neneqd 
 |-  ( ( B i^i A ) e. HAtoms -> -. ( B i^i A ) = 0H )
10 7 9 sylbi 
 |-  ( ( A i^i B ) e. HAtoms -> -. ( B i^i A ) = 0H )
11 atnssm0 
 |-  ( ( B e. CH /\ A e. HAtoms ) -> ( -. A C_ B <-> ( B i^i A ) = 0H ) )
12 11 ancoms 
 |-  ( ( A e. HAtoms /\ B e. CH ) -> ( -. A C_ B <-> ( B i^i A ) = 0H ) )
13 12 biimpd 
 |-  ( ( A e. HAtoms /\ B e. CH ) -> ( -. A C_ B -> ( B i^i A ) = 0H ) )
14 13 con1d 
 |-  ( ( A e. HAtoms /\ B e. CH ) -> ( -. ( B i^i A ) = 0H -> A C_ B ) )
15 10 14 syl5 
 |-  ( ( A e. HAtoms /\ B e. CH ) -> ( ( A i^i B ) e. HAtoms -> A C_ B ) )
16 5 15 impbid 
 |-  ( ( A e. HAtoms /\ B e. CH ) -> ( A C_ B <-> ( A i^i B ) e. HAtoms ) )