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

Metamath Proof Explorer

Theorem brsdom2

Description: Alternate definition of strict dominance. Definition 3 of Suppes p. 97. (Contributed by NM, 27-Jul-2004)

Ref Expression
Hypotheses brsdom2.1 
|- A e. _V
brsdom2.2 
|- B e. _V
Assertion brsdom2 
|- ( A ~< B <-> ( A ~<_ B /\ -. B ~<_ A ) )

Proof

Step Hyp Ref Expression
1 brsdom2.1 
 |-  A e. _V
2 brsdom2.2 
 |-  B e. _V
3 dfsdom2 
 |-  ~< = ( ~<_ \ `' ~<_ )
4 3 eleq2i 
 |-  ( <. A , B >. e. ~< <-> <. A , B >. e. ( ~<_ \ `' ~<_ ) )
5 df-br 
 |-  ( A ~< B <-> <. A , B >. e. ~< )
6 df-br 
 |-  ( A ~<_ B <-> <. A , B >. e. ~<_ )
7 df-br 
 |-  ( B ~<_ A <-> <. B , A >. e. ~<_ )
8 1 2 opelcnv 
 |-  ( <. A , B >. e. `' ~<_ <-> <. B , A >. e. ~<_ )
9 7 8 bitr4i 
 |-  ( B ~<_ A <-> <. A , B >. e. `' ~<_ )
10 9 notbii 
 |-  ( -. B ~<_ A <-> -. <. A , B >. e. `' ~<_ )
11 6 10 anbi12i 
 |-  ( ( A ~<_ B /\ -. B ~<_ A ) <-> ( <. A , B >. e. ~<_ /\ -. <. A , B >. e. `' ~<_ ) )
12 eldif 
 |-  ( <. A , B >. e. ( ~<_ \ `' ~<_ ) <-> ( <. A , B >. e. ~<_ /\ -. <. A , B >. e. `' ~<_ ) )
13 11 12 bitr4i 
 |-  ( ( A ~<_ B /\ -. B ~<_ A ) <-> <. A , B >. e. ( ~<_ \ `' ~<_ ) )
14 4 5 13 3bitr4i 
 |-  ( A ~< B <-> ( A ~<_ B /\ -. B ~<_ A ) )