Theorem sdomsdomcard

Description: A set strictly dominates iff its cardinal strictly dominates. (Contributed by NM, 30-Oct-2003)

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

Proof

Step	Hyp	Ref	Expression
1		relsdom	$$⊢\mathrm{Rel}\prec$$
2	1	brrelex2i	$$⊢A\prec B\to B\in \mathrm{V}$$
3		numth3	$$⊢B\in \mathrm{V}\to B\in \mathrm{dom}\mathrm{card}$$
4		cardid2	$$⊢B\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left(B\right)\approx B$$
5		ensym	$$⊢\mathrm{card}\left(B\right)\approx B\to B\approx \mathrm{card}\left(B\right)$$
6	2 3 4 5	4syl	$$⊢A\prec B\to B\approx \mathrm{card}\left(B\right)$$
7		sdomentr	$$⊢\left(A\prec B\wedge B\approx \mathrm{card}\left(B\right)\right)\to A\prec \mathrm{card}\left(B\right)$$
8	6 7	mpdan	$$⊢A\prec B\to A\prec \mathrm{card}\left(B\right)$$
9		sdomsdomcardi	$$⊢A\prec \mathrm{card}\left(B\right)\to A\prec B$$
10	8 9	impbii	$$⊢A\prec B\leftrightarrow A\prec \mathrm{card}\left(B\right)$$