Metamath Proof Explorer

Theorem atsseq

Description: Two atoms in a subset relationship are equal. (Contributed by NM, 26-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion atsseq 
|- ( ( A e. HAtoms /\ B e. HAtoms ) -> ( A C_ B <-> A = B ) )

Proof

Step Hyp Ref Expression
1 atne0 
 |-  ( A e. HAtoms -> A =/= 0H )
2 1 ad2antrr 
 |-  ( ( ( A e. HAtoms /\ B e. HAtoms ) /\ A C_ B ) -> A =/= 0H )
3 atelch 
 |-  ( A e. HAtoms -> A e. CH )
4 atss 
 |-  ( ( A e. CH /\ B e. HAtoms ) -> ( A C_ B -> ( A = B \/ A = 0H ) ) )
5 3 4 sylan 
 |-  ( ( A e. HAtoms /\ B e. HAtoms ) -> ( A C_ B -> ( A = B \/ A = 0H ) ) )
6 5 imp 
 |-  ( ( ( A e. HAtoms /\ B e. HAtoms ) /\ A C_ B ) -> ( A = B \/ A = 0H ) )
7 6 ord 
 |-  ( ( ( A e. HAtoms /\ B e. HAtoms ) /\ A C_ B ) -> ( -. A = B -> A = 0H ) )
8 7 necon1ad 
 |-  ( ( ( A e. HAtoms /\ B e. HAtoms ) /\ A C_ B ) -> ( A =/= 0H -> A = B ) )
9 2 8 mpd 
 |-  ( ( ( A e. HAtoms /\ B e. HAtoms ) /\ A C_ B ) -> A = B )
10 9 ex 
 |-  ( ( A e. HAtoms /\ B e. HAtoms ) -> ( A C_ B -> A = B ) )
11 eqimss 
 |-  ( A = B -> A C_ B )
12 10 11 impbid1 
 |-  ( ( A e. HAtoms /\ B e. HAtoms ) -> ( A C_ B <-> A = B ) )