Theorem wevonprcf1o

Description: If R is a set-like well-ordering of the universe and A is a proper class, then F is a bijection from the ordinals to A . This is the ZFC version of (4 -> 5) in https://tinyurl.com/hamkins-gblac . (Contributed by BTernaryTau, 9-Jun-2026)

	Ref	Expression
Hypothesis	wevonprcf1o.1	$$⊢F=OrdIso\left(R,A\right)$$
Assertion	wevonprcf1o	$$⊢\left(R\mathrm{We}\mathrm{V}\wedge R\mathrm{Se}\mathrm{V}\wedge \neg A\in \mathrm{V}\right)\to F:\mathrm{On}\underset{1-1\; onto}{⟶}A$$

Proof

Step	Hyp	Ref	Expression
1		wevonprcf1o.1	$$⊢F=OrdIso\left(R,A\right)$$
2		ssv	$$⊢A\subseteq \mathrm{V}$$
3		wess	$$⊢A\subseteq \mathrm{V}\to \left(R\mathrm{We}\mathrm{V}\to R\mathrm{We}A\right)$$
4	2 3	ax-mp	$$⊢R\mathrm{We}\mathrm{V}\to R\mathrm{We}A$$
5		sess2	$$⊢A\subseteq \mathrm{V}\to \left(R\mathrm{Se}\mathrm{V}\to R\mathrm{Se}A\right)$$
6	2 5	ax-mp	$$⊢R\mathrm{Se}\mathrm{V}\to R\mathrm{Se}A$$
7		id	$$⊢\neg A\in \mathrm{V}\to \neg A\in \mathrm{V}$$
8	4 6 7	3anim123i	$$⊢\left(R\mathrm{We}\mathrm{V}\wedge R\mathrm{Se}\mathrm{V}\wedge \neg A\in \mathrm{V}\right)\to \left(R\mathrm{We}A\wedge R\mathrm{Se}A\wedge \neg A\in \mathrm{V}\right)$$
9	1	ordtypeon	$$⊢\left(R\mathrm{We}A\wedge R\mathrm{Se}A\wedge \neg A\in \mathrm{V}\right)\to F{Isom}_{\mathrm{E},R}\left(\mathrm{On},A\right)$$
10		isof1o	$$⊢F{Isom}_{\mathrm{E},R}\left(\mathrm{On},A\right)\to F:\mathrm{On}\underset{1-1\; onto}{⟶}A$$
11	8 9 10	3syl	$$⊢\left(R\mathrm{We}\mathrm{V}\wedge R\mathrm{Se}\mathrm{V}\wedge \neg A\in \mathrm{V}\right)\to F:\mathrm{On}\underset{1-1\; onto}{⟶}A$$