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	$⊢ φ \to (\neg W \in V \to F : On \underset{1-1}{⟶} W)$
	onprcf1acwevd.2	$⊢ φ \to CHOICE$
	onprcf1acwevd.3	$⊢ W = \{r \| \exists x \in On (r \subseteq R_{1} (x) \times R_{1} (x) \land r We R_{1} (x))\}$
	onprcf1acwevd.4	$⊢ R = \{⟨y, z⟩ \| (rank (y) \in rank (z) \lor (rank (y) = rank (z) \land y S z))\}$
	onprcf1acwevd.5	$⊢ S = F (⋂ \{w \in On \| F (w) We R_{1} (suc rank (y))\})$
Assertion	onprcf1acwevd	$⊢ φ \to R We V$

Proof

Step	Hyp	Ref	Expression
1		onprcf1acwevd.1	$⊢ φ \to (\neg W \in V \to F : On \underset{1-1}{⟶} W)$
2		onprcf1acwevd.2	$⊢ φ \to CHOICE$
3		onprcf1acwevd.3	$⊢ W = \{r \| \exists x \in On (r \subseteq R_{1} (x) \times R_{1} (x) \land r We R_{1} (x))\}$
4		onprcf1acwevd.4	$⊢ R = \{⟨y, z⟩ \| (rank (y) \in rank (z) \lor (rank (y) = rank (z) \land y S z))\}$
5		onprcf1acwevd.5	$⊢ S = F (⋂ \{w \in On \| F (w) We R_{1} (suc rank (y))\})$
6		onprc	$⊢ \neg On \in V$
7	3	acwer1prc	$⊢ CHOICE \to \neg W \in V$
8	2 7	syl	$⊢ φ \to \neg W \in V$
9	8 1	mpd	$⊢ φ \to F : On \underset{1-1}{⟶} W$
10		f1f1orn	$⊢ F : On \underset{1-1}{⟶} W \to F : On \underset{1-1 onto}{⟶} ran F$
11		f1of1	$⊢ F : On \underset{1-1 onto}{⟶} ran F \to F : On \underset{1-1}{⟶} ran F$
12	9 10 11	3syl	$⊢ φ \to F : On \underset{1-1}{⟶} ran F$
13		f1dmex	$⊢ (F : On \underset{1-1}{⟶} ran F \land ran F \in V) \to On \in V$
14	12 13	sylan	$⊢ (φ \land ran F \in V) \to On \in V$
15	14	ex	$⊢ φ \to (ran F \in V \to On \in V)$
16	6 15	mtoi	$⊢ φ \to \neg ran F \in V$
17	16	adantr	$⊢ (φ \land v \in On) \to \neg ran F \in V$
18		f1f	$⊢ F : On \underset{1-1}{⟶} W \to F : On ⟶ W$
19	9 18	syl	$⊢ φ \to F : On ⟶ W$
20	19	frnd	$⊢ φ \to ran F \subseteq W$
21	3	onprcf1acwevdlem1	$⊢ (ran F \subseteq W \land v \in On \land \forall u \in ran F \neg u We R_{1} (v)) \to ran F \in V$
22	21	3expia	$⊢ (ran F \subseteq W \land v \in On) \to (\forall u \in ran F \neg u We R_{1} (v) \to ran F \in V)$
23	20 22	sylan	$⊢ (φ \land v \in On) \to (\forall u \in ran F \neg u We R_{1} (v) \to ran F \in V)$
24	17 23	mtod	$⊢ (φ \land v \in On) \to \neg \forall u \in ran F \neg u We R_{1} (v)$
25		dfrex2	$⊢ \exists u \in ran F u We R_{1} (v) \leftrightarrow \neg \forall u \in ran F \neg u We R_{1} (v)$
26	24 25	sylibr	$⊢ (φ \land v \in On) \to \exists u \in ran F u We R_{1} (v)$
27	19	ffnd	$⊢ φ \to F Fn On$
28		weeq1	$⊢ u = F (w) \to (u We R_{1} (v) \leftrightarrow F (w) We R_{1} (v))$
29	28	rexrn	$⊢ F Fn On \to (\exists u \in ran F u We R_{1} (v) \leftrightarrow \exists w \in On F (w) We R_{1} (v))$
30	27 29	syl	$⊢ φ \to (\exists u \in ran F u We R_{1} (v) \leftrightarrow \exists w \in On F (w) We R_{1} (v))$
31	30	adantr	$⊢ (φ \land v \in On) \to (\exists u \in ran F u We R_{1} (v) \leftrightarrow \exists w \in On F (w) We R_{1} (v))$
32	26 31	mpbid	$⊢ (φ \land v \in On) \to \exists w \in On F (w) We R_{1} (v)$
33	4 5 32	onprcf1acwevdlem2	$⊢ φ \to R We V$

Metamath Proof Explorer

Theorem onprcf1acwevd

Proof