Theorem dfac15

Description: Axiom of Choice equivalent: every set can be mapped one-to-one into the ordinals. (Contributed by BTernaryTau, 16-Sep-2026)

	Ref	Expression
Assertion	dfac15	$$⊢\mathrm{CHOICE}\leftrightarrow \forall x\exists ff:x\underset{1-1}{⟶}\mathrm{On}$$

Proof

Step	Hyp	Ref	Expression
1		dfac10c	$$⊢\mathrm{CHOICE}\leftrightarrow \forall x\exists v\in \mathrm{On}v\approx x$$
2		onss	$$⊢v\in \mathrm{On}\to v\subseteq \mathrm{On}$$
3		ensymb	$$⊢v\approx x\leftrightarrow x\approx v$$
4		bren	$$⊢x\approx v\leftrightarrow \exists ff:x\underset{1-1\; onto}{⟶}v$$
5	3 4	bitri	$$⊢v\approx x\leftrightarrow \exists ff:x\underset{1-1\; onto}{⟶}v$$
6		f1of1	$$⊢f:x\underset{1-1\; onto}{⟶}v\to f:x\underset{1-1}{⟶}v$$
7		f1ss	$$⊢\left(f:x\underset{1-1}{⟶}v\wedge v\subseteq \mathrm{On}\right)\to f:x\underset{1-1}{⟶}\mathrm{On}$$
8	6 7	sylan	$$⊢\left(f:x\underset{1-1\; onto}{⟶}v\wedge v\subseteq \mathrm{On}\right)\to f:x\underset{1-1}{⟶}\mathrm{On}$$
9	8	expcom	$$⊢v\subseteq \mathrm{On}\to \left(f:x\underset{1-1\; onto}{⟶}v\to f:x\underset{1-1}{⟶}\mathrm{On}\right)$$
10	9	eximdv	$$⊢v\subseteq \mathrm{On}\to \left(\exists ff:x\underset{1-1\; onto}{⟶}v\to \exists ff:x\underset{1-1}{⟶}\mathrm{On}\right)$$
11	5 10	biimtrid	$$⊢v\subseteq \mathrm{On}\to \left(v\approx x\to \exists ff:x\underset{1-1}{⟶}\mathrm{On}\right)$$
12	2 11	syl	$$⊢v\in \mathrm{On}\to \left(v\approx x\to \exists ff:x\underset{1-1}{⟶}\mathrm{On}\right)$$
13	12	rexlimiv	$$⊢\exists v\in \mathrm{On}v\approx x\to \exists ff:x\underset{1-1}{⟶}\mathrm{On}$$
14	13	alimi	$$⊢\forall x\exists v\in \mathrm{On}v\approx x\to \forall x\exists ff:x\underset{1-1}{⟶}\mathrm{On}$$
15	1 14	sylbi	$$⊢\mathrm{CHOICE}\to \forall x\exists ff:x\underset{1-1}{⟶}\mathrm{On}$$
16		eqid	$$⊢\left\{⟨y,z⟩|f\left(y\right)\in f\left(z\right)\right\}=\left\{⟨y,z⟩|f\left(y\right)\in f\left(z\right)\right\}$$
17	16	onf1we	$$⊢f:x\underset{1-1}{⟶}\mathrm{On}\to \left\{⟨y,z⟩|f\left(y\right)\in f\left(z\right)\right\}\mathrm{We}x$$
18		weinxp	$$⊢\left\{⟨y,z⟩|f\left(y\right)\in f\left(z\right)\right\}\mathrm{We}x\leftrightarrow \left(\left\{⟨y,z⟩|f\left(y\right)\in f\left(z\right)\right\}\cap \left(x\times x\right)\right)\mathrm{We}x$$
19		vex	$$⊢x\in \mathrm{V}$$
20	19 19	xpex	$$⊢x\times x\in \mathrm{V}$$
21	20	inex2	$$⊢\left\{⟨y,z⟩|f\left(y\right)\in f\left(z\right)\right\}\cap \left(x\times x\right)\in \mathrm{V}$$
22		weeq1	$$⊢w=\left\{⟨y,z⟩|f\left(y\right)\in f\left(z\right)\right\}\cap \left(x\times x\right)\to \left(w\mathrm{We}x\leftrightarrow \left(\left\{⟨y,z⟩|f\left(y\right)\in f\left(z\right)\right\}\cap \left(x\times x\right)\right)\mathrm{We}x\right)$$
23	21 22	spcev	$$⊢\left(\left\{⟨y,z⟩|f\left(y\right)\in f\left(z\right)\right\}\cap \left(x\times x\right)\right)\mathrm{We}x\to \exists ww\mathrm{We}x$$
24	18 23	sylbi	$$⊢\left\{⟨y,z⟩|f\left(y\right)\in f\left(z\right)\right\}\mathrm{We}x\to \exists ww\mathrm{We}x$$
25	17 24	syl	$$⊢f:x\underset{1-1}{⟶}\mathrm{On}\to \exists ww\mathrm{We}x$$
26	25	exlimiv	$$⊢\exists ff:x\underset{1-1}{⟶}\mathrm{On}\to \exists ww\mathrm{We}x$$
27	26	alimi	$$⊢\forall x\exists ff:x\underset{1-1}{⟶}\mathrm{On}\to \forall x\exists ww\mathrm{We}x$$
28		dfac8	$$⊢\mathrm{CHOICE}\leftrightarrow \forall x\exists ww\mathrm{We}x$$
29	27 28	sylibr	$$⊢\forall x\exists ff:x\underset{1-1}{⟶}\mathrm{On}\to \mathrm{CHOICE}$$
30	15 29	impbii	$$⊢\mathrm{CHOICE}\leftrightarrow \forall x\exists ff:x\underset{1-1}{⟶}\mathrm{On}$$