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 syl5ibr
 |-  ( ( 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 syl6ibr
 |-  ( ( 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 ) )