Theorem onprcf1of1orad

Description: If F is a bijection from the ordinals to the universe and H is a bijection from the ordinals to the proper class B , then I maps A one-to-one into B . This is the ZFC version of (5 -> 10) in https://tinyurl.com/hamkins-gblac in the case where one of the classes is a proper class. See onprcf1of1orbd for the case where neither class is a proper class, and see onprcf1of1ord for a theorem that covers both cases. Note that in NBG set theory the first two hypotheses would be replaced by something like ( ph -> A. X ( -. X e. _V -> E. F F : On -1-1-onto-> X ) ) . However, we cannot quantify over classes, so we split this into the case where X is the universe and the case where X is an arbitrary proper class B which together are sufficient for this proof. (Contributed by BTernaryTau, 17-Sep-2026)

	Ref	Expression
Hypotheses	onprcf1of1orad.1	$$⊢\phi \to F:\mathrm{On}\underset{1-1\; onto}{⟶}\mathrm{V}$$
	onprcf1of1orad.2	$$⊢\phi \to \left(\neg B\in \mathrm{V}\to H:\mathrm{On}\underset{1-1\; onto}{⟶}B\right)$$
	onprcf1of1orad.3	$$⊢\phi \to \neg B\in \mathrm{V}$$
	onprcf1of1orad.4	$$⊢I=H\circ \left({F^{-1}\upharpoonright }_A\right)$$
Assertion	onprcf1of1orad	$$⊢\phi \to I:A\underset{1-1}{⟶}B$$

Proof

Step	Hyp	Ref	Expression
1		onprcf1of1orad.1	$$⊢\phi \to F:\mathrm{On}\underset{1-1\; onto}{⟶}\mathrm{V}$$
2		onprcf1of1orad.2	$$⊢\phi \to \left(\neg B\in \mathrm{V}\to H:\mathrm{On}\underset{1-1\; onto}{⟶}B\right)$$
3		onprcf1of1orad.3	$$⊢\phi \to \neg B\in \mathrm{V}$$
4		onprcf1of1orad.4	$$⊢I=H\circ \left({F^{-1}\upharpoonright }_A\right)$$
5	3 2	mpd	$$⊢\phi \to H:\mathrm{On}\underset{1-1\; onto}{⟶}B$$
6		f1of1	$$⊢H:\mathrm{On}\underset{1-1\; onto}{⟶}B\to H:\mathrm{On}\underset{1-1}{⟶}B$$
7	5 6	syl	$$⊢\phi \to H:\mathrm{On}\underset{1-1}{⟶}B$$
8		f1ocnv	$$⊢F:\mathrm{On}\underset{1-1\; onto}{⟶}\mathrm{V}\to F^{-1}:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{On}$$
9		f1of1	$$⊢F^{-1}:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{On}\to F^{-1}:\mathrm{V}\underset{1-1}{⟶}\mathrm{On}$$
10		ssv	$$⊢A\subseteq \mathrm{V}$$
11		f1ssres	$$⊢\left(F^{-1}:\mathrm{V}\underset{1-1}{⟶}\mathrm{On}\wedge A\subseteq \mathrm{V}\right)\to \left({F^{-1}\upharpoonright }_A\right):A\underset{1-1}{⟶}\mathrm{On}$$
12	9 10 11	sylancl	$$⊢F^{-1}:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{On}\to \left({F^{-1}\upharpoonright }_A\right):A\underset{1-1}{⟶}\mathrm{On}$$
13	1 8 12	3syl	$$⊢\phi \to \left({F^{-1}\upharpoonright }_A\right):A\underset{1-1}{⟶}\mathrm{On}$$
14		f1co	$$⊢\left(H:\mathrm{On}\underset{1-1}{⟶}B\wedge \left({F^{-1}\upharpoonright }_A\right):A\underset{1-1}{⟶}\mathrm{On}\right)\to \left(H\circ \left({F^{-1}\upharpoonright }_A\right)\right):A\underset{1-1}{⟶}B$$
15	7 13 14	syl2anc	$$⊢\phi \to \left(H\circ \left({F^{-1}\upharpoonright }_A\right)\right):A\underset{1-1}{⟶}B$$
16		f1eq1	$$⊢I=H\circ \left({F^{-1}\upharpoonright }_A\right)\to \left(I:A\underset{1-1}{⟶}B\leftrightarrow \left(H\circ \left({F^{-1}\upharpoonright }_A\right)\right):A\underset{1-1}{⟶}B\right)$$
17	4 16	ax-mp	$$⊢I:A\underset{1-1}{⟶}B\leftrightarrow \left(H\circ \left({F^{-1}\upharpoonright }_A\right)\right):A\underset{1-1}{⟶}B$$
18	15 17	sylibr	$$⊢\phi \to I:A\underset{1-1}{⟶}B$$