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 bitrid
 |-  ( ( 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 ) )