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

Metamath Proof Explorer

Theorem sdomsdomcardi

Description: A set strictly dominates if its cardinal strictly dominates. (Contributed by Mario Carneiro, 13-Jan-2013)

Ref Expression
Assertion sdomsdomcardi 
|- ( A ~< ( card ` B ) -> A ~< B )

Proof

Step Hyp Ref Expression
1 sdom0 
 |-  -. A ~< (/)
2 ndmfv 
 |-  ( -. B e. dom card -> ( card ` B ) = (/) )
3 2 breq2d 
 |-  ( -. B e. dom card -> ( A ~< ( card ` B ) <-> A ~< (/) ) )
4 1 3 mtbiri 
 |-  ( -. B e. dom card -> -. A ~< ( card ` B ) )
5 4 con4i 
 |-  ( A ~< ( card ` B ) -> B e. dom card )
6 cardid2 
 |-  ( B e. dom card -> ( card ` B ) ~~ B )
7 5 6 syl 
 |-  ( A ~< ( card ` B ) -> ( card ` B ) ~~ B )
8 sdomentr 
 |-  ( ( A ~< ( card ` B ) /\ ( card ` B ) ~~ B ) -> A ~< B )
9 7 8 mpdan 
 |-  ( A ~< ( card ` B ) -> A ~< B )