Theorem onprcf1of1orbd

Description: If F is a bijection from the ordinals to the universe and both A and B are sets, then either A can be mapped one-to-one into B or B can be mapped one-to-one into A . This is the ZFC version of (5 -> 10) in https://tinyurl.com/hamkins-gblac in the case where neither class is a proper class. See onprcf1of1orad for the case where one of the classes is a proper class, and see onprcf1of1ord for a theorem that covers both cases. Note that in NBG set theory the first hypothesis would be replaced by something like ( ph -> A. X ( -. X e.V -> E. F F : On -1-1-onto-> X ) ) , but since we cannot quantify over classes, we instead consider only the case X = V which is sufficient for this proof. (Contributed by BTernaryTau, 17-Sep-2026)

	Ref	Expression
Hypotheses	onprcf1of1orbd.1	$$⊢\phi \to F:\mathrm{On}\underset{1-1\; onto}{⟶}\mathrm{V}$$
	onprcf1of1orbd.2	$$⊢\phi \to A\in V$$
	onprcf1of1orbd.3	$$⊢\phi \to B\in W$$
Assertion	onprcf1of1orbd	$$⊢\phi \to \left(\exists ff:A\underset{1-1}{⟶}B\vee \exists hh:B\underset{1-1}{⟶}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		onprcf1of1orbd.1	$$⊢\phi \to F:\mathrm{On}\underset{1-1\; onto}{⟶}\mathrm{V}$$
2		onprcf1of1orbd.2	$$⊢\phi \to A\in V$$
3		onprcf1of1orbd.3	$$⊢\phi \to B\in W$$
4		f1ocnv	$$⊢F:\mathrm{On}\underset{1-1\; onto}{⟶}\mathrm{V}\to F^{-1}:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{On}$$
5		f1ofun	$$⊢F^{-1}:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{On}\to \mathrm{Fun}{F}^{-1}$$
6		resfunexg	$$⊢\left(\mathrm{Fun}{F}^{-1}\wedge z\in \mathrm{V}\right)\to {F^{-1}\upharpoonright }_z\in \mathrm{V}$$
7	6	elvd	$$⊢\mathrm{Fun}{F}^{-1}\to {F^{-1}\upharpoonright }_z\in \mathrm{V}$$
8	4 5 7	3syl	$$⊢F:\mathrm{On}\underset{1-1\; onto}{⟶}\mathrm{V}\to {F^{-1}\upharpoonright }_z\in \mathrm{V}$$
9	1 8	syl	$$⊢\phi \to {F^{-1}\upharpoonright }_z\in \mathrm{V}$$
10		f1of1	$$⊢F^{-1}:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{On}\to F^{-1}:\mathrm{V}\underset{1-1}{⟶}\mathrm{On}$$
11		ssv	$$⊢z\subseteq \mathrm{V}$$
12		f1ssres	$$⊢\left(F^{-1}:\mathrm{V}\underset{1-1}{⟶}\mathrm{On}\wedge z\subseteq \mathrm{V}\right)\to \left({F^{-1}\upharpoonright }_z\right):z\underset{1-1}{⟶}\mathrm{On}$$
13	10 11 12	sylancl	$$⊢F^{-1}:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{On}\to \left({F^{-1}\upharpoonright }_z\right):z\underset{1-1}{⟶}\mathrm{On}$$
14	1 4 13	3syl	$$⊢\phi \to \left({F^{-1}\upharpoonright }_z\right):z\underset{1-1}{⟶}\mathrm{On}$$
15		f1eq1	$$⊢i={F^{-1}\upharpoonright }_z\to \left(i:z\underset{1-1}{⟶}\mathrm{On}\leftrightarrow \left({F^{-1}\upharpoonright }_z\right):z\underset{1-1}{⟶}\mathrm{On}\right)$$
16	9 14 15	spcedv	$$⊢\phi \to \exists ii:z\underset{1-1}{⟶}\mathrm{On}$$
17	16	alrimiv	$$⊢\phi \to \forall z\exists ii:z\underset{1-1}{⟶}\mathrm{On}$$
18		dfac15	$$⊢\mathrm{CHOICE}\leftrightarrow \forall z\exists ii:z\underset{1-1}{⟶}\mathrm{On}$$
19	17 18	sylibr	$$⊢\phi \to \mathrm{CHOICE}$$
20		dfac16	$$⊢\mathrm{CHOICE}\leftrightarrow \forall x\forall y\left(x\preccurlyeq y\vee y\preccurlyeq x\right)$$
21		breq2	$$⊢y=B\to \left(x\preccurlyeq y\leftrightarrow x\preccurlyeq B\right)$$
22		breq1	$$⊢y=B\to \left(y\preccurlyeq x\leftrightarrow B\preccurlyeq x\right)$$
23	21 22	orbi12d	$$⊢y=B\to \left(\left(x\preccurlyeq y\vee y\preccurlyeq x\right)\leftrightarrow \left(x\preccurlyeq B\vee B\preccurlyeq x\right)\right)$$
24	23	spcgv	$$⊢B\in W\to \left(\forall y\left(x\preccurlyeq y\vee y\preccurlyeq x\right)\to \left(x\preccurlyeq B\vee B\preccurlyeq x\right)\right)$$
25	3 24	syl	$$⊢\phi \to \left(\forall y\left(x\preccurlyeq y\vee y\preccurlyeq x\right)\to \left(x\preccurlyeq B\vee B\preccurlyeq x\right)\right)$$
26	25	alimdv	$$⊢\phi \to \left(\forall x\forall y\left(x\preccurlyeq y\vee y\preccurlyeq x\right)\to \forall x\left(x\preccurlyeq B\vee B\preccurlyeq x\right)\right)$$
27		breq1	$$⊢x=A\to \left(x\preccurlyeq B\leftrightarrow A\preccurlyeq B\right)$$
28		breq2	$$⊢x=A\to \left(B\preccurlyeq x\leftrightarrow B\preccurlyeq A\right)$$
29	27 28	orbi12d	$$⊢x=A\to \left(\left(x\preccurlyeq B\vee B\preccurlyeq x\right)\leftrightarrow \left(A\preccurlyeq B\vee B\preccurlyeq A\right)\right)$$
30	29	spcgv	$$⊢A\in V\to \left(\forall x\left(x\preccurlyeq B\vee B\preccurlyeq x\right)\to \left(A\preccurlyeq B\vee B\preccurlyeq A\right)\right)$$
31	2 26 30	sylsyld	$$⊢\phi \to \left(\forall x\forall y\left(x\preccurlyeq y\vee y\preccurlyeq x\right)\to \left(A\preccurlyeq B\vee B\preccurlyeq A\right)\right)$$
32	20 31	biimtrid	$$⊢\phi \to \left(\mathrm{CHOICE}\to \left(A\preccurlyeq B\vee B\preccurlyeq A\right)\right)$$
33	19 32	mpd	$$⊢\phi \to \left(A\preccurlyeq B\vee B\preccurlyeq A\right)$$
34		brdomg	$$⊢B\in W\to \left(A\preccurlyeq B\leftrightarrow \exists ff:A\underset{1-1}{⟶}B\right)$$
35	3 34	syl	$$⊢\phi \to \left(A\preccurlyeq B\leftrightarrow \exists ff:A\underset{1-1}{⟶}B\right)$$
36		brdomg	$$⊢A\in V\to \left(B\preccurlyeq A\leftrightarrow \exists hh:B\underset{1-1}{⟶}A\right)$$
37	2 36	syl	$$⊢\phi \to \left(B\preccurlyeq A\leftrightarrow \exists hh:B\underset{1-1}{⟶}A\right)$$
38	35 37	orbi12d	$$⊢\phi \to \left(\left(A\preccurlyeq B\vee B\preccurlyeq A\right)\leftrightarrow \left(\exists ff:A\underset{1-1}{⟶}B\vee \exists hh:B\underset{1-1}{⟶}A\right)\right)$$
39	33 38	mpbid	$$⊢\phi \to \left(\exists ff:A\underset{1-1}{⟶}B\vee \exists hh:B\underset{1-1}{⟶}A\right)$$