Theorem dfac16

Description: Axiom of Choice equivalent: for every pair of sets, one is dominated by the other (see also entri3 ). (Contributed by BTernaryTau, 17-Sep-2026)

	Ref	Expression
Assertion	dfac16	$$⊢\mathrm{CHOICE}\leftrightarrow \forall x\forall y\left(x\preccurlyeq y\vee y\preccurlyeq x\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfac10c	$$⊢\mathrm{CHOICE}\leftrightarrow \forall x\exists w\in \mathrm{On}w\approx x$$
2		dfac10c	$$⊢\mathrm{CHOICE}\leftrightarrow \forall y\exists z\in \mathrm{On}z\approx y$$
3		domtriord	$$⊢\left(w\in \mathrm{On}\wedge z\in \mathrm{On}\right)\to \left(w\preccurlyeq z\leftrightarrow \neg z\prec w\right)$$
4		xor3	$$⊢\neg \left(w\preccurlyeq z\leftrightarrow z\prec w\right)\leftrightarrow \left(w\preccurlyeq z\leftrightarrow \neg z\prec w\right)$$
5		nbior	$$⊢\neg \left(w\preccurlyeq z\leftrightarrow z\prec w\right)\to \left(w\preccurlyeq z\vee z\prec w\right)$$
6	4 5	sylbir	$$⊢\left(w\preccurlyeq z\leftrightarrow \neg z\prec w\right)\to \left(w\preccurlyeq z\vee z\prec w\right)$$
7	3 6	syl	$$⊢\left(w\in \mathrm{On}\wedge z\in \mathrm{On}\right)\to \left(w\preccurlyeq z\vee z\prec w\right)$$
8		ensym	$$⊢w\approx x\to x\approx w$$
9		endomtr	$$⊢\left(x\approx w\wedge w\preccurlyeq z\right)\to x\preccurlyeq z$$
10	8 9	sylan	$$⊢\left(w\approx x\wedge w\preccurlyeq z\right)\to x\preccurlyeq z$$
11	10	ex	$$⊢w\approx x\to \left(w\preccurlyeq z\to x\preccurlyeq z\right)$$
12		domentr	$$⊢\left(x\preccurlyeq z\wedge z\approx y\right)\to x\preccurlyeq y$$
13	12	expcom	$$⊢z\approx y\to \left(x\preccurlyeq z\to x\preccurlyeq y\right)$$
14	11 13	sylan9	$$⊢\left(w\approx x\wedge z\approx y\right)\to \left(w\preccurlyeq z\to x\preccurlyeq y\right)$$
15		ensym	$$⊢z\approx y\to y\approx z$$
16		sdomdom	$$⊢z\prec w\to z\preccurlyeq w$$
17		endomtr	$$⊢\left(y\approx z\wedge z\preccurlyeq w\right)\to y\preccurlyeq w$$
18	15 16 17	syl2an	$$⊢\left(z\approx y\wedge z\prec w\right)\to y\preccurlyeq w$$
19	18	ex	$$⊢z\approx y\to \left(z\prec w\to y\preccurlyeq w\right)$$
20		domentr	$$⊢\left(y\preccurlyeq w\wedge w\approx x\right)\to y\preccurlyeq x$$
21	20	expcom	$$⊢w\approx x\to \left(y\preccurlyeq w\to y\preccurlyeq x\right)$$
22	19 21	sylan9r	$$⊢\left(w\approx x\wedge z\approx y\right)\to \left(z\prec w\to y\preccurlyeq x\right)$$
23	14 22	orim12d	$$⊢\left(w\approx x\wedge z\approx y\right)\to \left(\left(w\preccurlyeq z\vee z\prec w\right)\to \left(x\preccurlyeq y\vee y\preccurlyeq x\right)\right)$$
24	7 23	mpan9	$$⊢\left(\left(w\in \mathrm{On}\wedge z\in \mathrm{On}\right)\wedge \left(w\approx x\wedge z\approx y\right)\right)\to \left(x\preccurlyeq y\vee y\preccurlyeq x\right)$$
25	24	an4s	$$⊢\left(\left(w\in \mathrm{On}\wedge w\approx x\right)\wedge \left(z\in \mathrm{On}\wedge z\approx y\right)\right)\to \left(x\preccurlyeq y\vee y\preccurlyeq x\right)$$
26	25	rexlimdvaa	$$⊢\left(w\in \mathrm{On}\wedge w\approx x\right)\to \left(\exists z\in \mathrm{On}z\approx y\to \left(x\preccurlyeq y\vee y\preccurlyeq x\right)\right)$$
27	26	alimdv	$$⊢\left(w\in \mathrm{On}\wedge w\approx x\right)\to \left(\forall y\exists z\in \mathrm{On}z\approx y\to \forall y\left(x\preccurlyeq y\vee y\preccurlyeq x\right)\right)$$
28	2 27	biimtrid	$$⊢\left(w\in \mathrm{On}\wedge w\approx x\right)\to \left(\mathrm{CHOICE}\to \forall y\left(x\preccurlyeq y\vee y\preccurlyeq x\right)\right)$$
29	28	rexlimiva	$$⊢\exists w\in \mathrm{On}w\approx x\to \left(\mathrm{CHOICE}\to \forall y\left(x\preccurlyeq y\vee y\preccurlyeq x\right)\right)$$
30	29	com12	$$⊢\mathrm{CHOICE}\to \left(\exists w\in \mathrm{On}w\approx x\to \forall y\left(x\preccurlyeq y\vee y\preccurlyeq x\right)\right)$$
31	30	alimdv	$$⊢\mathrm{CHOICE}\to \left(\forall x\exists w\in \mathrm{On}w\approx x\to \forall x\forall y\left(x\preccurlyeq y\vee y\preccurlyeq x\right)\right)$$
32	1 31	biimtrid	$$⊢\mathrm{CHOICE}\to \left(\mathrm{CHOICE}\to \forall x\forall y\left(x\preccurlyeq y\vee y\preccurlyeq x\right)\right)$$
33	32	pm2.43i	$$⊢\mathrm{CHOICE}\to \forall x\forall y\left(x\preccurlyeq y\vee y\preccurlyeq x\right)$$
34		breq2	$$⊢v=\mathrm{har}\left(x\right)\to \left(x\preccurlyeq v\leftrightarrow x\preccurlyeq \mathrm{har}\left(x\right)\right)$$
35		harcl	$$⊢\mathrm{har}\left(x\right)\in \mathrm{On}$$
36	35	a1i	$$⊢\forall y\left(x\preccurlyeq y\vee y\preccurlyeq x\right)\to \mathrm{har}\left(x\right)\in \mathrm{On}$$
37		fvex	$$⊢\mathrm{har}\left(x\right)\in \mathrm{V}$$
38		breq2	$$⊢y=\mathrm{har}\left(x\right)\to \left(x\preccurlyeq y\leftrightarrow x\preccurlyeq \mathrm{har}\left(x\right)\right)$$
39		breq1	$$⊢y=\mathrm{har}\left(x\right)\to \left(y\preccurlyeq x\leftrightarrow \mathrm{har}\left(x\right)\preccurlyeq x\right)$$
40	38 39	orbi12d	$$⊢y=\mathrm{har}\left(x\right)\to \left(\left(x\preccurlyeq y\vee y\preccurlyeq x\right)\leftrightarrow \left(x\preccurlyeq \mathrm{har}\left(x\right)\vee \mathrm{har}\left(x\right)\preccurlyeq x\right)\right)$$
41	37 40	spcv	$$⊢\forall y\left(x\preccurlyeq y\vee y\preccurlyeq x\right)\to \left(x\preccurlyeq \mathrm{har}\left(x\right)\vee \mathrm{har}\left(x\right)\preccurlyeq x\right)$$
42		harndom	$$⊢\neg \mathrm{har}\left(x\right)\preccurlyeq x$$
43	42	a1i	$$⊢\forall y\left(x\preccurlyeq y\vee y\preccurlyeq x\right)\to \neg \mathrm{har}\left(x\right)\preccurlyeq x$$
44	41 43	olcnd	$$⊢\forall y\left(x\preccurlyeq y\vee y\preccurlyeq x\right)\to x\preccurlyeq \mathrm{har}\left(x\right)$$
45	34 36 44	rspcedvdw	$$⊢\forall y\left(x\preccurlyeq y\vee y\preccurlyeq x\right)\to \exists v\in \mathrm{On}x\preccurlyeq v$$
46		ac10ct	$$⊢\exists v\in \mathrm{On}x\preccurlyeq v\to \exists rr\mathrm{We}x$$
47	45 46	syl	$$⊢\forall y\left(x\preccurlyeq y\vee y\preccurlyeq x\right)\to \exists rr\mathrm{We}x$$
48	47	alimi	$$⊢\forall x\forall y\left(x\preccurlyeq y\vee y\preccurlyeq x\right)\to \forall x\exists rr\mathrm{We}x$$
49		dfac8	$$⊢\mathrm{CHOICE}\leftrightarrow \forall x\exists rr\mathrm{We}x$$
50	48 49	sylibr	$$⊢\forall x\forall y\left(x\preccurlyeq y\vee y\preccurlyeq x\right)\to \mathrm{CHOICE}$$
51	33 50	impbii	$$⊢\mathrm{CHOICE}\leftrightarrow \forall x\forall y\left(x\preccurlyeq y\vee y\preccurlyeq x\right)$$