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	$⊢ φ \to (F : W \underset{1-1}{⟶} On \lor H : On \underset{1-1}{⟶} W)$
	onf1oracwevd.2	$⊢ φ \to \forall v (\exists f f : v \underset{1-1}{⟶} On \lor \exists h h : On \underset{1-1}{⟶} v)$
	onf1oracwevd.3	$⊢ W = \{r \| \exists x \in On (r \subseteq R_{1} (x) \times R_{1} (x) \land r We R_{1} (x))\}$
	onf1oracwevd.4	$⊢ R = \{⟨y, z⟩ \| (rank (y) \in rank (z) \lor (rank (y) = rank (z) \land y A z))\}$
	onf1oracwevd.5	$⊢ A = I (⋂ \{w \in On \| I (w) We R_{1} (suc rank (y))\})$
	onf1oracwevd.6	$⊢ I = if (F : W \underset{1-1}{⟶} On, F^{-1}, H)$
Assertion	onf1oracwevd	$⊢ φ \to R We V$

Proof

Step	Hyp	Ref	Expression
1		onf1oracwevd.1	$⊢ φ \to (F : W \underset{1-1}{⟶} On \lor H : On \underset{1-1}{⟶} W)$
2		onf1oracwevd.2	$⊢ φ \to \forall v (\exists f f : v \underset{1-1}{⟶} On \lor \exists h h : On \underset{1-1}{⟶} v)$
3		onf1oracwevd.3	$⊢ W = \{r \| \exists x \in On (r \subseteq R_{1} (x) \times R_{1} (x) \land r We R_{1} (x))\}$
4		onf1oracwevd.4	$⊢ R = \{⟨y, z⟩ \| (rank (y) \in rank (z) \lor (rank (y) = rank (z) \land y A z))\}$
5		onf1oracwevd.5	$⊢ A = I (⋂ \{w \in On \| I (w) We R_{1} (suc rank (y))\})$
6		onf1oracwevd.6	$⊢ I = if (F : W \underset{1-1}{⟶} On, F^{-1}, H)$
7		simpr	$⊢ (φ \land F : W \underset{1-1}{⟶} On) \to F : W \underset{1-1}{⟶} On$
8	7	a1d	$⊢ (φ \land F : W \underset{1-1}{⟶} On) \to (\neg W \in V \to F : W \underset{1-1}{⟶} On)$
9		onprc	$⊢ \neg On \in V$
10		f1dmex	$⊢ (h : On \underset{1-1}{⟶} v \land v \in V) \to On \in V$
11	10	elvd	$⊢ h : On \underset{1-1}{⟶} v \to On \in V$
12	9 11	mto	$⊢ \neg h : On \underset{1-1}{⟶} v$
13	12	nex	$⊢ \neg \exists h h : On \underset{1-1}{⟶} v$
14		orel2	$⊢ \neg \exists h h : On \underset{1-1}{⟶} v \to ((\exists f f : v \underset{1-1}{⟶} On \lor \exists h h : On \underset{1-1}{⟶} v) \to \exists f f : v \underset{1-1}{⟶} On)$
15	13 14	ax-mp	$⊢ (\exists f f : v \underset{1-1}{⟶} On \lor \exists h h : On \underset{1-1}{⟶} v) \to \exists f f : v \underset{1-1}{⟶} On$
16	2 15	sylg	$⊢ φ \to \forall v \exists f f : v \underset{1-1}{⟶} On$
17		dfac15	$⊢ CHOICE \leftrightarrow \forall v \exists f f : v \underset{1-1}{⟶} On$
18	16 17	sylibr	$⊢ φ \to CHOICE$
19	18	adantr	$⊢ (φ \land F : W \underset{1-1}{⟶} On) \to CHOICE$
20		eqid	$⊢ \{⟨y, z⟩ \| (rank (y) \in rank (z) \lor (rank (y) = rank (z) \land y F^{-1} (⋂ \{w \in On \| F^{-1} (w) We R_{1} (suc rank (y))\}) z))\} = \{⟨y, z⟩ \| (rank (y) \in rank (z) \lor (rank (y) = rank (z) \land y F^{-1} (⋂ \{w \in On \| F^{-1} (w) We R_{1} (suc rank (y))\}) z))\}$
21		eqid	$⊢ F^{-1} (⋂ \{w \in On \| F^{-1} (w) We R_{1} (suc rank (y))\}) = F^{-1} (⋂ \{w \in On \| F^{-1} (w) We R_{1} (suc rank (y))\})$
22	8 19 3 20 21	prconf1acwevd	$⊢ (φ \land F : W \underset{1-1}{⟶} On) \to \{⟨y, z⟩ \| (rank (y) \in rank (z) \lor (rank (y) = rank (z) \land y F^{-1} (⋂ \{w \in On \| F^{-1} (w) We R_{1} (suc rank (y))\}) z))\} We V$
23		iftrue	$⊢ F : W \underset{1-1}{⟶} On \to if (F : W \underset{1-1}{⟶} On, F^{-1}, H) = F^{-1}$
24	6 23	eqtrid	$⊢ F : W \underset{1-1}{⟶} On \to I = F^{-1}$
25	24	fveq1d	$⊢ F : W \underset{1-1}{⟶} On \to I (w) = F^{-1} (w)$
26		eqidd	$⊢ F : W \underset{1-1}{⟶} On \to R_{1} (suc rank (y)) = R_{1} (suc rank (y))$
27	25 26	weeq12d	$⊢ F : W \underset{1-1}{⟶} On \to (I (w) We R_{1} (suc rank (y)) \leftrightarrow F^{-1} (w) We R_{1} (suc rank (y)))$
28	27	rabbidv	$⊢ F : W \underset{1-1}{⟶} On \to \{w \in On \| I (w) We R_{1} (suc rank (y))\} = \{w \in On \| F^{-1} (w) We R_{1} (suc rank (y))\}$
29	28	inteqd	$⊢ F : W \underset{1-1}{⟶} On \to ⋂ \{w \in On \| I (w) We R_{1} (suc rank (y))\} = ⋂ \{w \in On \| F^{-1} (w) We R_{1} (suc rank (y))\}$
30	24 29	fveq12d	$⊢ F : W \underset{1-1}{⟶} On \to I (⋂ \{w \in On \| I (w) We R_{1} (suc rank (y))\}) = F^{-1} (⋂ \{w \in On \| F^{-1} (w) We R_{1} (suc rank (y))\})$
31	5 30	eqtrid	$⊢ F : W \underset{1-1}{⟶} On \to A = F^{-1} (⋂ \{w \in On \| F^{-1} (w) We R_{1} (suc rank (y))\})$
32	31	breqd	$⊢ F : W \underset{1-1}{⟶} On \to (y A z \leftrightarrow y F^{-1} (⋂ \{w \in On \| F^{-1} (w) We R_{1} (suc rank (y))\}) z)$
33	32	anbi2d	$⊢ F : W \underset{1-1}{⟶} On \to ((rank (y) = rank (z) \land y A z) \leftrightarrow (rank (y) = rank (z) \land y F^{-1} (⋂ \{w \in On \| F^{-1} (w) We R_{1} (suc rank (y))\}) z))$
34	33	orbi2d	$⊢ F : W \underset{1-1}{⟶} On \to ((rank (y) \in rank (z) \lor (rank (y) = rank (z) \land y A z)) \leftrightarrow (rank (y) \in rank (z) \lor (rank (y) = rank (z) \land y F^{-1} (⋂ \{w \in On \| F^{-1} (w) We R_{1} (suc rank (y))\}) z)))$
35	34	opabbidv	$⊢ F : W \underset{1-1}{⟶} On \to \{⟨y, z⟩ \| (rank (y) \in rank (z) \lor (rank (y) = rank (z) \land y A z))\} = \{⟨y, z⟩ \| (rank (y) \in rank (z) \lor (rank (y) = rank (z) \land y F^{-1} (⋂ \{w \in On \| F^{-1} (w) We R_{1} (suc rank (y))\}) z))\}$
36	4 35	eqtrid	$⊢ F : W \underset{1-1}{⟶} On \to R = \{⟨y, z⟩ \| (rank (y) \in rank (z) \lor (rank (y) = rank (z) \land y F^{-1} (⋂ \{w \in On \| F^{-1} (w) We R_{1} (suc rank (y))\}) z))\}$
37		eqidd	$⊢ F : W \underset{1-1}{⟶} On \to V = V$
38	36 37	weeq12d	$⊢ F : W \underset{1-1}{⟶} On \to (R We V \leftrightarrow \{⟨y, z⟩ \| (rank (y) \in rank (z) \lor (rank (y) = rank (z) \land y F^{-1} (⋂ \{w \in On \| F^{-1} (w) We R_{1} (suc rank (y))\}) z))\} We V)$
39	38	adantl	$⊢ (φ \land F : W \underset{1-1}{⟶} On) \to (R We V \leftrightarrow \{⟨y, z⟩ \| (rank (y) \in rank (z) \lor (rank (y) = rank (z) \land y F^{-1} (⋂ \{w \in On \| F^{-1} (w) We R_{1} (suc rank (y))\}) z))\} We V)$
40	22 39	mpbird	$⊢ (φ \land F : W \underset{1-1}{⟶} On) \to R We V$
41	1	orcanai	$⊢ (φ \land \neg F : W \underset{1-1}{⟶} On) \to H : On \underset{1-1}{⟶} W$
42		iffalse	$⊢ \neg F : W \underset{1-1}{⟶} On \to if (F : W \underset{1-1}{⟶} On, F^{-1}, H) = H$
43	6 42	eqtrid	$⊢ \neg F : W \underset{1-1}{⟶} On \to I = H$
44		f1eq1	$⊢ I = H \to (I : On \underset{1-1}{⟶} W \leftrightarrow H : On \underset{1-1}{⟶} W)$
45	43 44	syl	$⊢ \neg F : W \underset{1-1}{⟶} On \to (I : On \underset{1-1}{⟶} W \leftrightarrow H : On \underset{1-1}{⟶} W)$
46	45	adantl	$⊢ (φ \land \neg F : W \underset{1-1}{⟶} On) \to (I : On \underset{1-1}{⟶} W \leftrightarrow H : On \underset{1-1}{⟶} W)$
47	41 46	mpbird	$⊢ (φ \land \neg F : W \underset{1-1}{⟶} On) \to I : On \underset{1-1}{⟶} W$
48	47	a1d	$⊢ (φ \land \neg F : W \underset{1-1}{⟶} On) \to (\neg W \in V \to I : On \underset{1-1}{⟶} W)$
49	18	adantr	$⊢ (φ \land \neg F : W \underset{1-1}{⟶} On) \to CHOICE$
50	48 49 3 4 5	onprcf1acwevd	$⊢ (φ \land \neg F : W \underset{1-1}{⟶} On) \to R We V$
51	40 50	pm2.61dan	$⊢ φ \to R We V$

Metamath Proof Explorer

Theorem onf1oracwevd

Proof