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 )