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		df-ss	|- ( 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 ) )