prconf1acwevd

Description: If F maps the proper class W one-to-one into the ordinals and the Axiom of Choice holds, then R well-orders the universe. (Contributed by BTernaryTau, 16-Sep-2026)

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

Proof

Step	Hyp	Ref	Expression
1		prconf1acwevd.1	$⊢ φ \to (\neg W \in V \to F : W \underset{1-1}{⟶} On)$
2		prconf1acwevd.2	$⊢ φ \to CHOICE$
3		prconf1acwevd.3	$⊢ W = \{r \| \exists x \in On (r \subseteq R_{1} (x) \times R_{1} (x) \land r We R_{1} (x))\}$
4		prconf1acwevd.4	$⊢ R = \{⟨y, z⟩ \| (rank (y) \in rank (z) \lor (rank (y) = rank (z) \land y S z))\}$
5		prconf1acwevd.5	$⊢ S = F^{-1} (⋂ \{w \in On \| F^{-1} (w) We R_{1} (suc rank (y))\})$
6	3	acwer1prc	$⊢ CHOICE \to \neg W \in V$
7	2 6	syl	$⊢ φ \to \neg W \in V$
8	7 1	mpd	$⊢ φ \to F : W \underset{1-1}{⟶} On$
9		f1f	$⊢ F : W \underset{1-1}{⟶} On \to F : W ⟶ On$
10		frn	$⊢ F : W ⟶ On \to ran F \subseteq On$
11	8 9 10	3syl	$⊢ φ \to ran F \subseteq On$
12	11	adantr	$⊢ (φ \land v \in On) \to ran F \subseteq On$
13		ssid	$⊢ W \subseteq W$
14	3	onprcf1acwevdlem1	$⊢ (W \subseteq W \land v \in On \land \forall u \in W \neg u We R_{1} (v)) \to W \in V$
15	13 14	mp3an1	$⊢ (v \in On \land \forall u \in W \neg u We R_{1} (v)) \to W \in V$
16	15	ex	$⊢ v \in On \to (\forall u \in W \neg u We R_{1} (v) \to W \in V)$
17	16 7	nsyli	$⊢ v \in On \to (φ \to \neg \forall u \in W \neg u We R_{1} (v))$
18	17	impcom	$⊢ (φ \land v \in On) \to \neg \forall u \in W \neg u We R_{1} (v)$
19		dfrex2	$⊢ \exists u \in W u We R_{1} (v) \leftrightarrow \neg \forall u \in W \neg u We R_{1} (v)$
20	18 19	sylibr	$⊢ (φ \land v \in On) \to \exists u \in W u We R_{1} (v)$
21		f1f1orn	$⊢ F : W \underset{1-1}{⟶} On \to F : W \underset{1-1 onto}{⟶} ran F$
22		f1ocnv	$⊢ F : W \underset{1-1 onto}{⟶} ran F \to F^{-1} : ran F \underset{1-1 onto}{⟶} W$
23	8 21 22	3syl	$⊢ φ \to F^{-1} : ran F \underset{1-1 onto}{⟶} W$
24		f1ofo	$⊢ F^{-1} : ran F \underset{1-1 onto}{⟶} W \to F^{-1} : ran F \underset{onto}{⟶} W$
25		forn	$⊢ F^{-1} : ran F \underset{onto}{⟶} W \to ran F^{-1} = W$
26	23 24 25	3syl	$⊢ φ \to ran F^{-1} = W$
27	26	rexeqdv	$⊢ φ \to (\exists u \in ran F^{-1} u We R_{1} (v) \leftrightarrow \exists u \in W u We R_{1} (v))$
28		f1ofn	$⊢ F^{-1} : ran F \underset{1-1 onto}{⟶} W \to F^{-1} Fn ran F$
29		weeq1	$⊢ u = F^{-1} (w) \to (u We R_{1} (v) \leftrightarrow F^{-1} (w) We R_{1} (v))$
30	29	rexrn	$⊢ F^{-1} Fn ran F \to (\exists u \in ran F^{-1} u We R_{1} (v) \leftrightarrow \exists w \in ran F F^{-1} (w) We R_{1} (v))$
31	23 28 30	3syl	$⊢ φ \to (\exists u \in ran F^{-1} u We R_{1} (v) \leftrightarrow \exists w \in ran F F^{-1} (w) We R_{1} (v))$
32	27 31	bitr3d	$⊢ φ \to (\exists u \in W u We R_{1} (v) \leftrightarrow \exists w \in ran F F^{-1} (w) We R_{1} (v))$
33	32	adantr	$⊢ (φ \land v \in On) \to (\exists u \in W u We R_{1} (v) \leftrightarrow \exists w \in ran F F^{-1} (w) We R_{1} (v))$
34	20 33	mpbid	$⊢ (φ \land v \in On) \to \exists w \in ran F F^{-1} (w) We R_{1} (v)$
35		ssrexv	$⊢ ran F \subseteq On \to (\exists w \in ran F F^{-1} (w) We R_{1} (v) \to \exists w \in On F^{-1} (w) We R_{1} (v))$
36	12 34 35	sylc	$⊢ (φ \land v \in On) \to \exists w \in On F^{-1} (w) We R_{1} (v)$
37	4 5 36	onprcf1acwevdlem2	$⊢ φ \to R We V$

Metamath Proof Explorer

Theorem prconf1acwevd

Proof