Metamath Proof Explorer

Theorem domtri2

Description: Trichotomy of dominance for numerable sets (does not use AC). (Contributed by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion domtri2 
|- ( ( A e. dom card /\ B e. dom card ) -> ( A ~<_ B <-> -. B ~< A ) )

Proof

Step Hyp Ref Expression
1 carddom2 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( ( card ` A ) C_ ( card ` B ) <-> A ~<_ B ) )
2 cardon 
 |-  ( card ` A ) e. On
3 cardon 
 |-  ( card ` B ) e. On
4 ontri1 
 |-  ( ( ( card ` A ) e. On /\ ( card ` B ) e. On ) -> ( ( card ` A ) C_ ( card ` B ) <-> -. ( card ` B ) e. ( card ` A ) ) )
5 2 3 4 mp2an 
 |-  ( ( card ` A ) C_ ( card ` B ) <-> -. ( card ` B ) e. ( card ` A ) )
6 cardsdom2 
 |-  ( ( B e. dom card /\ A e. dom card ) -> ( ( card ` B ) e. ( card ` A ) <-> B ~< A ) )
7 6 ancoms 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( ( card ` B ) e. ( card ` A ) <-> B ~< A ) )
8 7 notbid 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( -. ( card ` B ) e. ( card ` A ) <-> -. B ~< A ) )
9 5 8 syl5bb 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( ( card ` A ) C_ ( card ` B ) <-> -. B ~< A ) )
10 1 9 bitr3d 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( A ~<_ B <-> -. B ~< A ) )