Theorem fodomacn

Description: A version of fodom that doesn't require the Axiom of Choice ax-ac . If A has choice sequences of length B , then any surjection from A to B can be inverted to an injection the other way. (Contributed by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Assertion	fodomacn	$$⊢A\in \underset{\_}{\mathrm{AC}}B\to \left(F:A\underset{onto}{⟶}B\to B\preccurlyeq A\right)$$

Proof

Step	Hyp	Ref	Expression
1		foelrn	$$⊢\left(F:A\underset{onto}{⟶}B\wedge x\in B\right)\to \exists y\in Ax=F\left(y\right)$$
2	1	ralrimiva	$$⊢F:A\underset{onto}{⟶}B\to \forall x\in B\exists y\in Ax=F\left(y\right)$$
3		fveq2	$$⊢y=f\left(x\right)\to F\left(y\right)=F\left(f\left(x\right)\right)$$
4	3	eqeq2d	$$⊢y=f\left(x\right)\to \left(x=F\left(y\right)\leftrightarrow x=F\left(f\left(x\right)\right)\right)$$
5	4	acni3	$$⊢\left(A\in \underset{\_}{\mathrm{AC}}B\wedge \forall x\in B\exists y\in Ax=F\left(y\right)\right)\to \exists f\left(f:B⟶A\wedge \forall x\in Bx=F\left(f\left(x\right)\right)\right)$$
6	2 5	sylan2	$$⊢\left(A\in \underset{\_}{\mathrm{AC}}B\wedge F:A\underset{onto}{⟶}B\right)\to \exists f\left(f:B⟶A\wedge \forall x\in Bx=F\left(f\left(x\right)\right)\right)$$
7		simpll	$$⊢\left(\left(A\in \underset{\_}{\mathrm{AC}}B\wedge F:A\underset{onto}{⟶}B\right)\wedge \left(f:B⟶A\wedge \forall x\in Bx=F\left(f\left(x\right)\right)\right)\right)\to A\in \underset{\_}{\mathrm{AC}}B$$
8		acnrcl	$$⊢A\in \underset{\_}{\mathrm{AC}}B\to B\in \mathrm{V}$$
9	7 8	syl	$$⊢\left(\left(A\in \underset{\_}{\mathrm{AC}}B\wedge F:A\underset{onto}{⟶}B\right)\wedge \left(f:B⟶A\wedge \forall x\in Bx=F\left(f\left(x\right)\right)\right)\right)\to B\in \mathrm{V}$$
10		simprl	$$⊢\left(\left(A\in \underset{\_}{\mathrm{AC}}B\wedge F:A\underset{onto}{⟶}B\right)\wedge \left(f:B⟶A\wedge \forall x\in Bx=F\left(f\left(x\right)\right)\right)\right)\to f:B⟶A$$
11		fveq2	$$⊢f\left(y\right)=f\left(z\right)\to F\left(f\left(y\right)\right)=F\left(f\left(z\right)\right)$$
12		simprr	$$⊢\left(\left(A\in \underset{\_}{\mathrm{AC}}B\wedge F:A\underset{onto}{⟶}B\right)\wedge \left(f:B⟶A\wedge \forall x\in Bx=F\left(f\left(x\right)\right)\right)\right)\to \forall x\in Bx=F\left(f\left(x\right)\right)$$
13		id	$$⊢x=y\to x=y$$
14		2fveq3	$$⊢x=y\to F\left(f\left(x\right)\right)=F\left(f\left(y\right)\right)$$
15	13 14	eqeq12d	$$⊢x=y\to \left(x=F\left(f\left(x\right)\right)\leftrightarrow y=F\left(f\left(y\right)\right)\right)$$
16	15	rspccva	$$⊢\left(\forall x\in Bx=F\left(f\left(x\right)\right)\wedge y\in B\right)\to y=F\left(f\left(y\right)\right)$$
17		id	$$⊢x=z\to x=z$$
18		2fveq3	$$⊢x=z\to F\left(f\left(x\right)\right)=F\left(f\left(z\right)\right)$$
19	17 18	eqeq12d	$$⊢x=z\to \left(x=F\left(f\left(x\right)\right)\leftrightarrow z=F\left(f\left(z\right)\right)\right)$$
20	19	rspccva	$$⊢\left(\forall x\in Bx=F\left(f\left(x\right)\right)\wedge z\in B\right)\to z=F\left(f\left(z\right)\right)$$
21	16 20	eqeqan12d	$$⊢\left(\left(\forall x\in Bx=F\left(f\left(x\right)\right)\wedge y\in B\right)\wedge \left(\forall x\in Bx=F\left(f\left(x\right)\right)\wedge z\in B\right)\right)\to \left(y=z\leftrightarrow F\left(f\left(y\right)\right)=F\left(f\left(z\right)\right)\right)$$
22	21	anandis	$$⊢\left(\forall x\in Bx=F\left(f\left(x\right)\right)\wedge \left(y\in B\wedge z\in B\right)\right)\to \left(y=z\leftrightarrow F\left(f\left(y\right)\right)=F\left(f\left(z\right)\right)\right)$$
23	12 22	sylan	$$⊢\left(\left(\left(A\in \underset{\_}{\mathrm{AC}}B\wedge F:A\underset{onto}{⟶}B\right)\wedge \left(f:B⟶A\wedge \forall x\in Bx=F\left(f\left(x\right)\right)\right)\right)\wedge \left(y\in B\wedge z\in B\right)\right)\to \left(y=z\leftrightarrow F\left(f\left(y\right)\right)=F\left(f\left(z\right)\right)\right)$$
24	11 23	syl5ibr	$$⊢\left(\left(\left(A\in \underset{\_}{\mathrm{AC}}B\wedge F:A\underset{onto}{⟶}B\right)\wedge \left(f:B⟶A\wedge \forall x\in Bx=F\left(f\left(x\right)\right)\right)\right)\wedge \left(y\in B\wedge z\in B\right)\right)\to \left(f\left(y\right)=f\left(z\right)\to y=z\right)$$
25	24	ralrimivva	$$⊢\left(\left(A\in \underset{\_}{\mathrm{AC}}B\wedge F:A\underset{onto}{⟶}B\right)\wedge \left(f:B⟶A\wedge \forall x\in Bx=F\left(f\left(x\right)\right)\right)\right)\to \forall y\in B\forall z\in B\left(f\left(y\right)=f\left(z\right)\to y=z\right)$$
26		dff13	$$⊢f:B\underset{1-1}{⟶}A\leftrightarrow \left(f:B⟶A\wedge \forall y\in B\forall z\in B\left(f\left(y\right)=f\left(z\right)\to y=z\right)\right)$$
27	10 25 26	sylanbrc	$$⊢\left(\left(A\in \underset{\_}{\mathrm{AC}}B\wedge F:A\underset{onto}{⟶}B\right)\wedge \left(f:B⟶A\wedge \forall x\in Bx=F\left(f\left(x\right)\right)\right)\right)\to f:B\underset{1-1}{⟶}A$$
28		f1dom2g	$$⊢\left(B\in \mathrm{V}\wedge A\in \underset{\_}{\mathrm{AC}}B\wedge f:B\underset{1-1}{⟶}A\right)\to B\preccurlyeq A$$
29	9 7 27 28	syl3anc	$$⊢\left(\left(A\in \underset{\_}{\mathrm{AC}}B\wedge F:A\underset{onto}{⟶}B\right)\wedge \left(f:B⟶A\wedge \forall x\in Bx=F\left(f\left(x\right)\right)\right)\right)\to B\preccurlyeq A$$
30	6 29	exlimddv	$$⊢\left(A\in \underset{\_}{\mathrm{AC}}B\wedge F:A\underset{onto}{⟶}B\right)\to B\preccurlyeq A$$
31	30	ex	$$⊢A\in \underset{\_}{\mathrm{AC}}B\to \left(F:A\underset{onto}{⟶}B\to B\preccurlyeq A\right)$$