Theorem sdomsdomcardi

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

	Ref	Expression
Assertion	sdomsdomcardi	$$⊢A\prec \mathrm{card}\left(B\right)\to A\prec B$$

Proof

Step	Hyp	Ref	Expression
1		sdom0	$$⊢\neg A\prec \varnothing$$
2		ndmfv	$$⊢\neg B\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left(B\right)=\varnothing$$
3	2	breq2d	$$⊢\neg B\in \mathrm{dom}\mathrm{card}\to \left(A\prec \mathrm{card}\left(B\right)\leftrightarrow A\prec \varnothing \right)$$
4	1 3	mtbiri	$$⊢\neg B\in \mathrm{dom}\mathrm{card}\to \neg A\prec \mathrm{card}\left(B\right)$$
5	4	con4i	$$⊢A\prec \mathrm{card}\left(B\right)\to B\in \mathrm{dom}\mathrm{card}$$
6		cardid2	$$⊢B\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left(B\right)\approx B$$
7	5 6	syl	$$⊢A\prec \mathrm{card}\left(B\right)\to \mathrm{card}\left(B\right)\approx B$$
8		sdomentr	$$⊢\left(A\prec \mathrm{card}\left(B\right)\wedge \mathrm{card}\left(B\right)\approx B\right)\to A\prec B$$
9	7 8	mpdan	$$⊢A\prec \mathrm{card}\left(B\right)\to A\prec B$$