This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem brdom2

Description: Dominance in terms of strict dominance and equinumerosity. Theorem 22(iv) of Suppes p. 97. (Contributed by NM, 17-Jun-1998)

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

Proof

Step Hyp Ref Expression
1 dfdom2 
 |-  ~<_ = ( ~< u. ~~ )
2 1 eleq2i 
 |-  ( <. A , B >. e. ~<_ <-> <. A , B >. e. ( ~< u. ~~ ) )
3 df-br 
 |-  ( A ~<_ B <-> <. A , B >. e. ~<_ )
4 df-br 
 |-  ( A ~< B <-> <. A , B >. e. ~< )
5 df-br 
 |-  ( A ~~ B <-> <. A , B >. e. ~~ )
6 4 5 orbi12i 
 |-  ( ( A ~< B \/ A ~~ B ) <-> ( <. A , B >. e. ~< \/ <. A , B >. e. ~~ ) )
7 elun 
 |-  ( <. A , B >. e. ( ~< u. ~~ ) <-> ( <. A , B >. e. ~< \/ <. A , B >. e. ~~ ) )
8 6 7 bitr4i 
 |-  ( ( A ~< B \/ A ~~ B ) <-> <. A , B >. e. ( ~< u. ~~ ) )
9 2 3 8 3bitr4i 
 |-  ( A ~<_ B <-> ( A ~< B \/ A ~~ B ) )