Theorem fodomnum

Description: A version of fodom that doesn't require the Axiom of Choice ax-ac . (Contributed by Mario Carneiro, 28-Feb-2013) (Revised by Mario Carneiro, 28-Apr-2015)

	Ref	Expression
Assertion	fodomnum	$$⊢A\in \mathrm{dom}\mathrm{card}\to \left(F:A\underset{onto}{⟶}B\to B\preccurlyeq A\right)$$

Proof

Step	Hyp	Ref	Expression
1		focdmex	$$⊢A\in \mathrm{dom}\mathrm{card}\to \left(F:A\underset{onto}{⟶}B\to B\in \mathrm{V}\right)$$
2	1	com12	$$⊢F:A\underset{onto}{⟶}B\to \left(A\in \mathrm{dom}\mathrm{card}\to B\in \mathrm{V}\right)$$
3		numacn	$$⊢B\in \mathrm{V}\to \left(A\in \mathrm{dom}\mathrm{card}\to A\in \underset{\_}{\mathrm{AC}}B\right)$$
4	2 3	syli	$$⊢F:A\underset{onto}{⟶}B\to \left(A\in \mathrm{dom}\mathrm{card}\to A\in \underset{\_}{\mathrm{AC}}B\right)$$
5	4	com12	$$⊢A\in \mathrm{dom}\mathrm{card}\to \left(F:A\underset{onto}{⟶}B\to A\in \underset{\_}{\mathrm{AC}}B\right)$$
6		fodomacn	$$⊢A\in \underset{\_}{\mathrm{AC}}B\to \left(F:A\underset{onto}{⟶}B\to B\preccurlyeq A\right)$$
7	5 6	syli	$$⊢A\in \mathrm{dom}\mathrm{card}\to \left(F:A\underset{onto}{⟶}B\to B\preccurlyeq A\right)$$