Metamath Proof Explorer


Theorem brsdom

Description: Strict dominance relation, meaning " B is strictly greater in size than A ". Definition of Mendelson p. 255. (Contributed by NM, 25-Jun-1998)

Ref Expression
Assertion brsdom ABAB¬AB

Proof

Step Hyp Ref Expression
1 df-sdom =
2 1 eleq2i ABAB
3 df-br ABAB
4 df-br ABAB
5 df-br ABAB
6 5 notbii ¬AB¬AB
7 4 6 anbi12i AB¬ABAB¬AB
8 eldif ABAB¬AB
9 7 8 bitr4i AB¬ABAB
10 2 3 9 3bitr4i ABAB¬AB