Theorem onf1oracwevd 35964

Description: If 𝐹 maps the proper class 𝑊 one-to-one into the ordinals or 𝐻 maps the ordinals one-to-one into the proper class 𝑊, 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 𝑅 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 (𝜑 → ∀𝑋(∃𝐹𝐹:𝑋–1-1→On ∨ ∃𝐻𝐻:On–1-1→𝑋)). However, we cannot quantify over classes, so we split this into the case where 𝑋 is a set and the case where 𝑋 is the proper class 𝑊 which together are sufficient for this proof. (Contributed by BTernaryTau, 16-Sep-2026.)

Hypotheses

Ref	Expression
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

Ref	Expression
onf1oracwevd	⊢ (𝜑 → 𝑅 We V)

Distinct variable groups:   𝜑,𝑦   𝑧,𝐴   𝑣,𝑓   𝑥,𝑟   𝑤,𝐹,𝑦,𝑧   𝑤,𝐼,𝑦,𝑧   𝑤,𝑊,𝑦,𝑧

Allowed substitution hints:   𝜑(𝑥, 𝑧, 𝑤, 𝑣, 𝑓, ℎ, 𝑟)   𝐴(𝑥, 𝑦, 𝑤, 𝑣, 𝑓, ℎ, 𝑟)   𝑅(𝑥, 𝑦, 𝑧, 𝑤, 𝑣, 𝑓, ℎ, 𝑟)   𝐹(𝑥, 𝑣, 𝑓, ℎ, 𝑟)   𝐻(𝑥, 𝑦, 𝑧, 𝑤, 𝑣, 𝑓, ℎ, 𝑟)   𝐼(𝑥, 𝑣, 𝑓, ℎ, 𝑟)   𝑊(𝑥, 𝑣, 𝑓, ℎ, 𝑟)

Proof of Theorem onf1oracwevd

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861  ∀wal 1567   = wceq 1569  ∃wex 1811   ∈ wcel 2144  {cab 2738  ∃wrex 3086  {crab 3412  Vcvv 3450   ⊆ wss 3895  ifcif 4481  ∩ cint 4906   class class class wbr 5102  {copab 5166   We wwe 5602   × cxp 5648  ^◡ccnv 5649  Oncon0 6362  suc csuc 6364  –1-1→wf1 6535  ‘cfv 6538  𝑅₁cr1 9767  rankcrnk 9768  CHOICEwac 10195

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-reg 9587  ax-inf2 9643

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-tp 4588  df-op 4590  df-uni 4867  df-int 4907  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-se 5604  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-isom 6547  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-rpss 7739  df-om 7878  df-1st 8001  df-2nd 8002  df-frecs 8300  df-wrecs 8331  df-smo 8355  df-recs 8380  df-rdg 8419  df-seqom 8459  df-1o 8477  df-2o 8478  df-er 8718  df-map 8850  df-en 8975  df-dom 8976  df-sdom 8977  df-fin 8978  df-oi 9505  df-wdom 9560  df-r1 9769  df-rank 9770  df-dju 9983  df-card 10021  df-ac 10196  df-fin2 10365  df-fin4 10366  df-fin3 10367  df-fin5 10368  df-fin6 10369  df-fin7 10370

This theorem is used by: (None)