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

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 
|- ( A ~< B <-> ( A ~<_ B /\ -. A ~~ B ) )

Proof

Step Hyp Ref Expression
1 df-sdom 
 |-  ~< = ( ~<_ \ ~~ )
2 1 eleq2i 
 |-  ( <. A , B >. e. ~< <-> <. A , B >. e. ( ~<_ \ ~~ ) )
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 5 notbii 
 |-  ( -. A ~~ B <-> -. <. A , B >. e. ~~ )
7 4 6 anbi12i 
 |-  ( ( A ~<_ B /\ -. A ~~ B ) <-> ( <. A , B >. e. ~<_ /\ -. <. A , B >. e. ~~ ) )
8 eldif 
 |-  ( <. A , B >. e. ( ~<_ \ ~~ ) <-> ( <. A , B >. e. ~<_ /\ -. <. A , B >. e. ~~ ) )
9 7 8 bitr4i 
 |-  ( ( A ~<_ B /\ -. A ~~ B ) <-> <. A , B >. e. ( ~<_ \ ~~ ) )
10 2 3 9 3bitr4i 
 |-  ( A ~< B <-> ( A ~<_ B /\ -. A ~~ B ) )