Metamath Proof Explorer


Theorem bren2

Description: Equinumerosity expressed in terms of dominance and strict dominance. (Contributed by NM, 23-Oct-2004)

Ref Expression
Assertion bren2
|- ( A ~~ B <-> ( A ~<_ B /\ -. A ~< B ) )

Proof

Step Hyp Ref Expression
1 endom
 |-  ( A ~~ B -> A ~<_ B )
2 sdomnen
 |-  ( A ~< B -> -. A ~~ B )
3 2 con2i
 |-  ( A ~~ B -> -. A ~< B )
4 1 3 jca
 |-  ( A ~~ B -> ( A ~<_ B /\ -. A ~< B ) )
5 brdom2
 |-  ( A ~<_ B <-> ( A ~< B \/ A ~~ B ) )
6 5 biimpi
 |-  ( A ~<_ B -> ( A ~< B \/ A ~~ B ) )
7 6 orcanai
 |-  ( ( A ~<_ B /\ -. A ~< B ) -> A ~~ B )
8 4 7 impbii
 |-  ( A ~~ B <-> ( A ~<_ B /\ -. A ~< B ) )