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

Metamath Proof Explorer

Theorem fidomtri2

Description: Trichotomy of dominance without AC when one set is finite. (Contributed by Stefan O'Rear, 30-Oct-2014) (Revised by Mario Carneiro, 7-May-2015)

Ref Expression
Assertion fidomtri2 
|- ( ( A e. V /\ B e. Fin ) -> ( A ~<_ B <-> -. B ~< A ) )

Proof

Step Hyp Ref Expression
1 domnsym 
 |-  ( A ~<_ B -> -. B ~< A )
2 sdomdom 
 |-  ( A ~< B -> A ~<_ B )
3 2 con3i 
 |-  ( -. A ~<_ B -> -. A ~< B )
4 fidomtri 
 |-  ( ( B e. Fin /\ A e. V ) -> ( B ~<_ A <-> -. A ~< B ) )
5 4 ancoms 
 |-  ( ( A e. V /\ B e. Fin ) -> ( B ~<_ A <-> -. A ~< B ) )
6 3 5 imbitrrid 
 |-  ( ( A e. V /\ B e. Fin ) -> ( -. A ~<_ B -> B ~<_ A ) )
7 ensym 
 |-  ( B ~~ A -> A ~~ B )
8 endom 
 |-  ( A ~~ B -> A ~<_ B )
9 7 8 syl 
 |-  ( B ~~ A -> A ~<_ B )
10 9 con3i 
 |-  ( -. A ~<_ B -> -. B ~~ A )
11 6 10 jca2 
 |-  ( ( A e. V /\ B e. Fin ) -> ( -. A ~<_ B -> ( B ~<_ A /\ -. B ~~ A ) ) )
12 brsdom 
 |-  ( B ~< A <-> ( B ~<_ A /\ -. B ~~ A ) )
13 11 12 imbitrrdi 
 |-  ( ( A e. V /\ B e. Fin ) -> ( -. A ~<_ B -> B ~< A ) )
14 13 con1d 
 |-  ( ( A e. V /\ B e. Fin ) -> ( -. B ~< A -> A ~<_ B ) )
15 1 14 impbid2 
 |-  ( ( A e. V /\ B e. Fin ) -> ( A ~<_ B <-> -. B ~< A ) )