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	⊢ ( 𝜑 → ( ¬ 𝑊 ∈ V → 𝐹 : On –1-1→ 𝑊 ) )
	onprcf1acwevd.2	⊢ ( 𝜑 → CHOICE )
	onprcf1acwevd.3	⊢ 𝑊 = { 𝑟 ∣ ∃ 𝑥 ∈ On ( 𝑟 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑟 We ( 𝑅1 ‘ 𝑥 ) ) }
	onprcf1acwevd.4	⊢ 𝑅 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝑧 ) ∨ ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ∧ 𝑦 𝑆 𝑧 ) ) }
	onprcf1acwevd.5	⊢ 𝑆 = ( 𝐹 ‘ ∩ { 𝑤 ∈ On ∣ ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } )
Assertion	onprcf1acwevd	⊢ ( 𝜑 → 𝑅 We V )

Proof

Step	Hyp	Ref	Expression
1		onprcf1acwevd.1	⊢ ( 𝜑 → ( ¬ 𝑊 ∈ V → 𝐹 : On –1-1→ 𝑊 ) )
2		onprcf1acwevd.2	⊢ ( 𝜑 → CHOICE )
3		onprcf1acwevd.3	⊢ 𝑊 = { 𝑟 ∣ ∃ 𝑥 ∈ On ( 𝑟 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑟 We ( 𝑅1 ‘ 𝑥 ) ) }
4		onprcf1acwevd.4	⊢ 𝑅 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝑧 ) ∨ ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ∧ 𝑦 𝑆 𝑧 ) ) }
5		onprcf1acwevd.5	⊢ 𝑆 = ( 𝐹 ‘ ∩ { 𝑤 ∈ On ∣ ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } )
6		onprc	⊢ ¬ On ∈ V
7	3	acwer1prc	⊢ ( CHOICE → ¬ 𝑊 ∈ V )
8	2 7	syl	⊢ ( 𝜑 → ¬ 𝑊 ∈ V )
9	8 1	mpd	⊢ ( 𝜑 → 𝐹 : On –1-1→ 𝑊 )
10		f1f1orn	⊢ ( 𝐹 : On –1-1→ 𝑊 → 𝐹 : On –1-1-onto→ ran 𝐹 )
11		f1of1	⊢ ( 𝐹 : On –1-1-onto→ ran 𝐹 → 𝐹 : On –1-1→ ran 𝐹 )
12	9 10 11	3syl	⊢ ( 𝜑 → 𝐹 : On –1-1→ ran 𝐹 )
13		f1dmex	⊢ ( ( 𝐹 : On –1-1→ ran 𝐹 ∧ ran 𝐹 ∈ V ) → On ∈ V )
14	12 13	sylan	⊢ ( ( 𝜑 ∧ ran 𝐹 ∈ V ) → On ∈ V )
15	14	ex	⊢ ( 𝜑 → ( ran 𝐹 ∈ V → On ∈ V ) )
16	6 15	mtoi	⊢ ( 𝜑 → ¬ ran 𝐹 ∈ V )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ On ) → ¬ ran 𝐹 ∈ V )
18		f1f	⊢ ( 𝐹 : On –1-1→ 𝑊 → 𝐹 : On ⟶ 𝑊 )
19	9 18	syl	⊢ ( 𝜑 → 𝐹 : On ⟶ 𝑊 )
20	19	frnd	⊢ ( 𝜑 → ran 𝐹 ⊆ 𝑊 )
21	3	onprcf1acwevdlem1	⊢ ( ( ran 𝐹 ⊆ 𝑊 ∧ 𝑣 ∈ On ∧ ∀ 𝑢 ∈ ran 𝐹 ¬ 𝑢 We ( 𝑅1 ‘ 𝑣 ) ) → ran 𝐹 ∈ V )
22	21	3expia	⊢ ( ( ran 𝐹 ⊆ 𝑊 ∧ 𝑣 ∈ On ) → ( ∀ 𝑢 ∈ ran 𝐹 ¬ 𝑢 We ( 𝑅1 ‘ 𝑣 ) → ran 𝐹 ∈ V ) )
23	20 22	sylan	⊢ ( ( 𝜑 ∧ 𝑣 ∈ On ) → ( ∀ 𝑢 ∈ ran 𝐹 ¬ 𝑢 We ( 𝑅1 ‘ 𝑣 ) → ran 𝐹 ∈ V ) )
24	17 23	mtod	⊢ ( ( 𝜑 ∧ 𝑣 ∈ On ) → ¬ ∀ 𝑢 ∈ ran 𝐹 ¬ 𝑢 We ( 𝑅1 ‘ 𝑣 ) )
25		dfrex2	⊢ ( ∃ 𝑢 ∈ ran 𝐹 𝑢 We ( 𝑅1 ‘ 𝑣 ) ↔ ¬ ∀ 𝑢 ∈ ran 𝐹 ¬ 𝑢 We ( 𝑅1 ‘ 𝑣 ) )
26	24 25	sylibr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ On ) → ∃ 𝑢 ∈ ran 𝐹 𝑢 We ( 𝑅1 ‘ 𝑣 ) )
27	19	ffnd	⊢ ( 𝜑 → 𝐹 Fn On )
28		weeq1	⊢ ( 𝑢 = ( 𝐹 ‘ 𝑤 ) → ( 𝑢 We ( 𝑅1 ‘ 𝑣 ) ↔ ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ 𝑣 ) ) )
29	28	rexrn	⊢ ( 𝐹 Fn On → ( ∃ 𝑢 ∈ ran 𝐹 𝑢 We ( 𝑅1 ‘ 𝑣 ) ↔ ∃ 𝑤 ∈ On ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ 𝑣 ) ) )
30	27 29	syl	⊢ ( 𝜑 → ( ∃ 𝑢 ∈ ran 𝐹 𝑢 We ( 𝑅1 ‘ 𝑣 ) ↔ ∃ 𝑤 ∈ On ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ 𝑣 ) ) )
31	30	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ On ) → ( ∃ 𝑢 ∈ ran 𝐹 𝑢 We ( 𝑅1 ‘ 𝑣 ) ↔ ∃ 𝑤 ∈ On ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ 𝑣 ) ) )
32	26 31	mpbid	⊢ ( ( 𝜑 ∧ 𝑣 ∈ On ) → ∃ 𝑤 ∈ On ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ 𝑣 ) )
33	4 5 32	onprcf1acwevdlem2	⊢ ( 𝜑 → 𝑅 We V )