Theorem onprcf1acwevd

Description: If F maps the ordinals one-to-one into the proper class W and the Axiom of Choice holds, then R well-orders the universe. This is the ZFC version of (7 -> 3) in https://tinyurl.com/hamkins-gblac . Note that in NBG set theory the first hypothesis would be something like ( ph -> A. X ( -. X e. _V -> E. F F : On -1-1-> X ) ) , but since we cannot quantify over classes, we instead consider only the case X = W which is sufficient for this proof. (Contributed by BTernaryTau, 16-Sep-2026)

	Ref	Expression
Hypotheses	onprcf1acwevd.1	|- ( ph -> ( -. W e. _V -> F : On -1-1-> W ) )
	onprcf1acwevd.2	|- ( ph -> CHOICE )
	onprcf1acwevd.3	|- W = { r | E. x e. On ( r C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ r We ( R1 ` x ) ) }
	onprcf1acwevd.4	|- R = { <. y , z >. | ( ( rank ` y ) e. ( rank ` z ) \/ ( ( rank ` y ) = ( rank ` z ) /\ y S z ) ) }
	onprcf1acwevd.5	|- S = ( F ` |^| { w e. On | ( F ` w ) We ( R1 ` suc ( rank ` y ) ) } )
Assertion	onprcf1acwevd	|- ( ph -> R We _V )

Proof

Step	Hyp	Ref	Expression
1		onprcf1acwevd.1	|- ( ph -> ( -. W e. _V -> F : On -1-1-> W ) )
2		onprcf1acwevd.2	|- ( ph -> CHOICE )
3		onprcf1acwevd.3	|- W = { r | E. x e. On ( r C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ r We ( R1 ` x ) ) }
4		onprcf1acwevd.4	|- R = { <. y , z >. | ( ( rank ` y ) e. ( rank ` z ) \/ ( ( rank ` y ) = ( rank ` z ) /\ y S z ) ) }
5		onprcf1acwevd.5	|- S = ( F ` |^| { w e. On | ( F ` w ) We ( R1 ` suc ( rank ` y ) ) } )
6		onprc	|- -. On e. _V
7	3	acwer1prc	|- ( CHOICE -> -. W e. _V )
8	2 7	syl	|- ( ph -> -. W e. _V )
9	8 1	mpd	|- ( ph -> F : On -1-1-> W )
10		f1f1orn	|- ( F : On -1-1-> W -> F : On -1-1-onto-> ran F )
11		f1of1	|- ( F : On -1-1-onto-> ran F -> F : On -1-1-> ran F )
12	9 10 11	3syl	|- ( ph -> F : On -1-1-> ran F )
13		f1dmex	|- ( ( F : On -1-1-> ran F /\ ran F e. _V ) -> On e. _V )
14	12 13	sylan	|- ( ( ph /\ ran F e. _V ) -> On e. _V )
15	14	ex	|- ( ph -> ( ran F e. _V -> On e. _V ) )
16	6 15	mtoi	|- ( ph -> -. ran F e. _V )
17	16	adantr	|- ( ( ph /\ v e. On ) -> -. ran F e. _V )
18		f1f	|- ( F : On -1-1-> W -> F : On --> W )
19	9 18	syl	|- ( ph -> F : On --> W )
20	19	frnd	|- ( ph -> ran F C_ W )
21	3	onprcf1acwevdlem1	|- ( ( ran F C_ W /\ v e. On /\ A. u e. ran F -. u We ( R1 ` v ) ) -> ran F e. _V )
22	21	3expia	|- ( ( ran F C_ W /\ v e. On ) -> ( A. u e. ran F -. u We ( R1 ` v ) -> ran F e. _V ) )
23	20 22	sylan	|- ( ( ph /\ v e. On ) -> ( A. u e. ran F -. u We ( R1 ` v ) -> ran F e. _V ) )
24	17 23	mtod	|- ( ( ph /\ v e. On ) -> -. A. u e. ran F -. u We ( R1 ` v ) )
25		dfrex2	|- ( E. u e. ran F u We ( R1 ` v ) <-> -. A. u e. ran F -. u We ( R1 ` v ) )
26	24 25	sylibr	|- ( ( ph /\ v e. On ) -> E. u e. ran F u We ( R1 ` v ) )
27	19	ffnd	|- ( ph -> F Fn On )
28		weeq1	|- ( u = ( F ` w ) -> ( u We ( R1 ` v ) <-> ( F ` w ) We ( R1 ` v ) ) )
29	28	rexrn	|- ( F Fn On -> ( E. u e. ran F u We ( R1 ` v ) <-> E. w e. On ( F ` w ) We ( R1 ` v ) ) )
30	27 29	syl	|- ( ph -> ( E. u e. ran F u We ( R1 ` v ) <-> E. w e. On ( F ` w ) We ( R1 ` v ) ) )
31	30	adantr	|- ( ( ph /\ v e. On ) -> ( E. u e. ran F u We ( R1 ` v ) <-> E. w e. On ( F ` w ) We ( R1 ` v ) ) )
32	26 31	mpbid	|- ( ( ph /\ v e. On ) -> E. w e. On ( F ` w ) We ( R1 ` v ) )
33	4 5 32	onprcf1acwevdlem2	|- ( ph -> R We _V )