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 ) ) |
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 ) ) |