Theorem onf1oracwevd

Description: If F maps the proper class W one-to-one into the ordinals or H maps the ordinals one-to-one into the proper class W , and if every set can either be mapped one-to-one into the ordinals or have the ordinals mapped one-to-one into it, then R well-orders the universe. This is the ZFC version of (9 -> 3) in https://tinyurl.com/hamkins-gblac . Note that in NBG set theory the first two hypotheses would be replaced by something like ( ph -> A. X ( E. F F : X -1-1-> On \/ E. H H : On -1-1-> X ) ) . However, we cannot quantify over classes, so we split this into the case where X is a set and the case where X is the proper class W which together are sufficient for this proof. (Contributed by BTernaryTau, 16-Sep-2026)

	Ref	Expression
Hypotheses	onf1oracwevd.1	⊢ ( 𝜑 → ( 𝐹 : 𝑊 –1-1→ On ∨ 𝐻 : On –1-1→ 𝑊 ) )
	onf1oracwevd.2	⊢ ( 𝜑 → ∀ 𝑣 ( ∃ 𝑓 𝑓 : 𝑣 –1-1→ On ∨ ∃ ℎ ℎ : On –1-1→ 𝑣 ) )
	onf1oracwevd.3	⊢ 𝑊 = { 𝑟 ∣ ∃ 𝑥 ∈ On ( 𝑟 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑟 We ( 𝑅1 ‘ 𝑥 ) ) }
	onf1oracwevd.4	⊢ 𝑅 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝑧 ) ∨ ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ∧ 𝑦 𝐴 𝑧 ) ) }
	onf1oracwevd.5	⊢ 𝐴 = ( 𝐼 ‘ ∩ { 𝑤 ∈ On ∣ ( 𝐼 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } )
	onf1oracwevd.6	⊢ 𝐼 = if ( 𝐹 : 𝑊 –1-1→ On , ◡ 𝐹 , 𝐻 )
Assertion	onf1oracwevd	⊢ ( 𝜑 → 𝑅 We V )

Proof

Step	Hyp	Ref	Expression
1		onf1oracwevd.1	⊢ ( 𝜑 → ( 𝐹 : 𝑊 –1-1→ On ∨ 𝐻 : On –1-1→ 𝑊 ) )
2		onf1oracwevd.2	⊢ ( 𝜑 → ∀ 𝑣 ( ∃ 𝑓 𝑓 : 𝑣 –1-1→ On ∨ ∃ ℎ ℎ : On –1-1→ 𝑣 ) )
3		onf1oracwevd.3	⊢ 𝑊 = { 𝑟 ∣ ∃ 𝑥 ∈ On ( 𝑟 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑟 We ( 𝑅1 ‘ 𝑥 ) ) }
4		onf1oracwevd.4	⊢ 𝑅 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝑧 ) ∨ ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ∧ 𝑦 𝐴 𝑧 ) ) }
5		onf1oracwevd.5	⊢ 𝐴 = ( 𝐼 ‘ ∩ { 𝑤 ∈ On ∣ ( 𝐼 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } )
6		onf1oracwevd.6	⊢ 𝐼 = if ( 𝐹 : 𝑊 –1-1→ On , ◡ 𝐹 , 𝐻 )
7		simpr	⊢ ( ( 𝜑 ∧ 𝐹 : 𝑊 –1-1→ On ) → 𝐹 : 𝑊 –1-1→ On )
8	7	a1d	⊢ ( ( 𝜑 ∧ 𝐹 : 𝑊 –1-1→ On ) → ( ¬ 𝑊 ∈ V → 𝐹 : 𝑊 –1-1→ On ) )
9		onprc	⊢ ¬ On ∈ V
10		f1dmex	⊢ ( ( ℎ : On –1-1→ 𝑣 ∧ 𝑣 ∈ V ) → On ∈ V )
11	10	elvd	⊢ ( ℎ : On –1-1→ 𝑣 → On ∈ V )
12	9 11	mto	⊢ ¬ ℎ : On –1-1→ 𝑣
13	12	nex	⊢ ¬ ∃ ℎ ℎ : On –1-1→ 𝑣
14		orel2	⊢ ( ¬ ∃ ℎ ℎ : On –1-1→ 𝑣 → ( ( ∃ 𝑓 𝑓 : 𝑣 –1-1→ On ∨ ∃ ℎ ℎ : On –1-1→ 𝑣 ) → ∃ 𝑓 𝑓 : 𝑣 –1-1→ On ) )
15	13 14	ax-mp	⊢ ( ( ∃ 𝑓 𝑓 : 𝑣 –1-1→ On ∨ ∃ ℎ ℎ : On –1-1→ 𝑣 ) → ∃ 𝑓 𝑓 : 𝑣 –1-1→ On )
16	2 15	sylg	⊢ ( 𝜑 → ∀ 𝑣 ∃ 𝑓 𝑓 : 𝑣 –1-1→ On )
17		dfac15	⊢ ( CHOICE ↔ ∀ 𝑣 ∃ 𝑓 𝑓 : 𝑣 –1-1→ On )
18	16 17	sylibr	⊢ ( 𝜑 → CHOICE )
19	18	adantr	⊢ ( ( 𝜑 ∧ 𝐹 : 𝑊 –1-1→ On ) → CHOICE )
20		eqid	⊢ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝑧 ) ∨ ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ∧ 𝑦 ( ◡ 𝐹 ‘ ∩ { 𝑤 ∈ On ∣ ( ◡ 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } ) 𝑧 ) ) } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝑧 ) ∨ ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ∧ 𝑦 ( ◡ 𝐹 ‘ ∩ { 𝑤 ∈ On ∣ ( ◡ 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } ) 𝑧 ) ) }
21		eqid	⊢ ( ◡ 𝐹 ‘ ∩ { 𝑤 ∈ On ∣ ( ◡ 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } ) = ( ◡ 𝐹 ‘ ∩ { 𝑤 ∈ On ∣ ( ◡ 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } )
22	8 19 3 20 21	prconf1acwevd	⊢ ( ( 𝜑 ∧ 𝐹 : 𝑊 –1-1→ On ) → { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝑧 ) ∨ ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ∧ 𝑦 ( ◡ 𝐹 ‘ ∩ { 𝑤 ∈ On ∣ ( ◡ 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } ) 𝑧 ) ) } We V )
23		iftrue	⊢ ( 𝐹 : 𝑊 –1-1→ On → if ( 𝐹 : 𝑊 –1-1→ On , ◡ 𝐹 , 𝐻 ) = ◡ 𝐹 )
24	6 23	eqtrid	⊢ ( 𝐹 : 𝑊 –1-1→ On → 𝐼 = ◡ 𝐹 )
25	24	fveq1d	⊢ ( 𝐹 : 𝑊 –1-1→ On → ( 𝐼 ‘ 𝑤 ) = ( ◡ 𝐹 ‘ 𝑤 ) )
26		eqidd	⊢ ( 𝐹 : 𝑊 –1-1→ On → ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) = ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) )
27	25 26	weeq12d	⊢ ( 𝐹 : 𝑊 –1-1→ On → ( ( 𝐼 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ↔ ( ◡ 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ) )
28	27	rabbidv	⊢ ( 𝐹 : 𝑊 –1-1→ On → { 𝑤 ∈ On ∣ ( 𝐼 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } = { 𝑤 ∈ On ∣ ( ◡ 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } )
29	28	inteqd	⊢ ( 𝐹 : 𝑊 –1-1→ On → ∩ { 𝑤 ∈ On ∣ ( 𝐼 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } = ∩ { 𝑤 ∈ On ∣ ( ◡ 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } )
30	24 29	fveq12d	⊢ ( 𝐹 : 𝑊 –1-1→ On → ( 𝐼 ‘ ∩ { 𝑤 ∈ On ∣ ( 𝐼 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } ) = ( ◡ 𝐹 ‘ ∩ { 𝑤 ∈ On ∣ ( ◡ 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } ) )
31	5 30	eqtrid	⊢ ( 𝐹 : 𝑊 –1-1→ On → 𝐴 = ( ◡ 𝐹 ‘ ∩ { 𝑤 ∈ On ∣ ( ◡ 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } ) )
32	31	breqd	⊢ ( 𝐹 : 𝑊 –1-1→ On → ( 𝑦 𝐴 𝑧 ↔ 𝑦 ( ◡ 𝐹 ‘ ∩ { 𝑤 ∈ On ∣ ( ◡ 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } ) 𝑧 ) )
33	32	anbi2d	⊢ ( 𝐹 : 𝑊 –1-1→ On → ( ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ∧ 𝑦 𝐴 𝑧 ) ↔ ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ∧ 𝑦 ( ◡ 𝐹 ‘ ∩ { 𝑤 ∈ On ∣ ( ◡ 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } ) 𝑧 ) ) )
34	33	orbi2d	⊢ ( 𝐹 : 𝑊 –1-1→ On → ( ( ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝑧 ) ∨ ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ∧ 𝑦 𝐴 𝑧 ) ) ↔ ( ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝑧 ) ∨ ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ∧ 𝑦 ( ◡ 𝐹 ‘ ∩ { 𝑤 ∈ On ∣ ( ◡ 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } ) 𝑧 ) ) ) )
35	34	opabbidv	⊢ ( 𝐹 : 𝑊 –1-1→ On → { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝑧 ) ∨ ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ∧ 𝑦 𝐴 𝑧 ) ) } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝑧 ) ∨ ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ∧ 𝑦 ( ◡ 𝐹 ‘ ∩ { 𝑤 ∈ On ∣ ( ◡ 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } ) 𝑧 ) ) } )
36	4 35	eqtrid	⊢ ( 𝐹 : 𝑊 –1-1→ On → 𝑅 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝑧 ) ∨ ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ∧ 𝑦 ( ◡ 𝐹 ‘ ∩ { 𝑤 ∈ On ∣ ( ◡ 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } ) 𝑧 ) ) } )
37		eqidd	⊢ ( 𝐹 : 𝑊 –1-1→ On → V = V )
38	36 37	weeq12d	⊢ ( 𝐹 : 𝑊 –1-1→ On → ( 𝑅 We V ↔ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝑧 ) ∨ ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ∧ 𝑦 ( ◡ 𝐹 ‘ ∩ { 𝑤 ∈ On ∣ ( ◡ 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } ) 𝑧 ) ) } We V ) )
39	38	adantl	⊢ ( ( 𝜑 ∧ 𝐹 : 𝑊 –1-1→ On ) → ( 𝑅 We V ↔ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝑧 ) ∨ ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ∧ 𝑦 ( ◡ 𝐹 ‘ ∩ { 𝑤 ∈ On ∣ ( ◡ 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } ) 𝑧 ) ) } We V ) )
40	22 39	mpbird	⊢ ( ( 𝜑 ∧ 𝐹 : 𝑊 –1-1→ On ) → 𝑅 We V )
41	1	orcanai	⊢ ( ( 𝜑 ∧ ¬ 𝐹 : 𝑊 –1-1→ On ) → 𝐻 : On –1-1→ 𝑊 )
42		iffalse	⊢ ( ¬ 𝐹 : 𝑊 –1-1→ On → if ( 𝐹 : 𝑊 –1-1→ On , ◡ 𝐹 , 𝐻 ) = 𝐻 )
43	6 42	eqtrid	⊢ ( ¬ 𝐹 : 𝑊 –1-1→ On → 𝐼 = 𝐻 )
44		f1eq1	⊢ ( 𝐼 = 𝐻 → ( 𝐼 : On –1-1→ 𝑊 ↔ 𝐻 : On –1-1→ 𝑊 ) )
45	43 44	syl	⊢ ( ¬ 𝐹 : 𝑊 –1-1→ On → ( 𝐼 : On –1-1→ 𝑊 ↔ 𝐻 : On –1-1→ 𝑊 ) )
46	45	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝐹 : 𝑊 –1-1→ On ) → ( 𝐼 : On –1-1→ 𝑊 ↔ 𝐻 : On –1-1→ 𝑊 ) )
47	41 46	mpbird	⊢ ( ( 𝜑 ∧ ¬ 𝐹 : 𝑊 –1-1→ On ) → 𝐼 : On –1-1→ 𝑊 )
48	47	a1d	⊢ ( ( 𝜑 ∧ ¬ 𝐹 : 𝑊 –1-1→ On ) → ( ¬ 𝑊 ∈ V → 𝐼 : On –1-1→ 𝑊 ) )
49	18	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐹 : 𝑊 –1-1→ On ) → CHOICE )
50	48 49 3 4 5	onprcf1acwevd	⊢ ( ( 𝜑 ∧ ¬ 𝐹 : 𝑊 –1-1→ On ) → 𝑅 We V )
51	40 50	pm2.61dan	⊢ ( 𝜑 → 𝑅 We V )