onvfowev

Description: If F maps the ordinals onto the universe, then R well-orders the universe. This is the ZFC version of (8 -> 3) in https://tinyurl.com/hamkins-gblac . Note that in NBG set theory the antecedent would be something like A. X ( X =/= (/) -> E. F F : On -onto-> X ) , but since we cannot quantify over classes, we instead consider only the case X = _V which is sufficient for this proof. (Contributed by BTernaryTau, 12-Jun-2026)

	Ref	Expression
Hypotheses	onvfowev.1	$⊢ R = \{⟨x, y⟩ \| H (x) \in H (y)\}$
	onvfowev.2	$⊢ H = (z \in V ⟼ ⋂ F^{-1} [\{z\}])$
Assertion	onvfowev	$⊢ F : On \underset{onto}{⟶} V \to R We V$

Proof

Step	Hyp	Ref	Expression
1		onvfowev.1	$⊢ R = \{⟨x, y⟩ \| H (x) \in H (y)\}$
2		onvfowev.2	$⊢ H = (z \in V ⟼ ⋂ F^{-1} [\{z\}])$
3		cnvimass	$⊢ F^{-1} [\{z\}] \subseteq dom F$
4		fofn	$⊢ F : On \underset{onto}{⟶} V \to F Fn On$
5	4	fndmd	$⊢ F : On \underset{onto}{⟶} V \to dom F = On$
6	3 5	sseqtrid	$⊢ F : On \underset{onto}{⟶} V \to F^{-1} [\{z\}] \subseteq On$
7		vex	$⊢ z \in V$
8		forn	$⊢ F : On \underset{onto}{⟶} V \to ran F = V$
9	7 8	eleqtrrid	$⊢ F : On \underset{onto}{⟶} V \to z \in ran F$
10		inisegn0	$⊢ z \in ran F \leftrightarrow F^{-1} [\{z\}] \neq \emptyset$
11	9 10	sylib	$⊢ F : On \underset{onto}{⟶} V \to F^{-1} [\{z\}] \neq \emptyset$
12		oninton	$⊢ (F^{-1} [\{z\}] \subseteq On \land F^{-1} [\{z\}] \neq \emptyset) \to ⋂ F^{-1} [\{z\}] \in On$
13	6 11 12	syl2anc	$⊢ F : On \underset{onto}{⟶} V \to ⋂ F^{-1} [\{z\}] \in On$
14	13	adantr	$⊢ (F : On \underset{onto}{⟶} V \land z \in V) \to ⋂ F^{-1} [\{z\}] \in On$
15	14 2	fmptd	$⊢ F : On \underset{onto}{⟶} V \to H : V ⟶ On$
16		fofun	$⊢ F : On \underset{onto}{⟶} V \to Fun F$
17		fvexd	$⊢ (F : On \underset{onto}{⟶} V \land H (v) = H (w)) \to H (v) \in V$
18		vex	$⊢ w \in V$
19	18	a1i	$⊢ F : On \underset{onto}{⟶} V \to w \in V$
20	13	adantr	$⊢ (F : On \underset{onto}{⟶} V \land z = w) \to ⋂ F^{-1} [\{z\}] \in On$
21		sneq	$⊢ z = w \to \{z\} = \{w\}$
22	21	imaeq2d	$⊢ z = w \to F^{-1} [\{z\}] = F^{-1} [\{w\}]$
23	22	inteqd	$⊢ z = w \to ⋂ F^{-1} [\{z\}] = ⋂ F^{-1} [\{w\}]$
24	23	adantl	$⊢ (F : On \underset{onto}{⟶} V \land z = w) \to ⋂ F^{-1} [\{z\}] = ⋂ F^{-1} [\{w\}]$
25	19 20 24	fvmptdv2	$⊢ F : On \underset{onto}{⟶} V \to (H = (z \in V ⟼ ⋂ F^{-1} [\{z\}]) \to H (w) = ⋂ F^{-1} [\{w\}])$
26	2 25	mpi	$⊢ F : On \underset{onto}{⟶} V \to H (w) = ⋂ F^{-1} [\{w\}]$
27		cnvimass	$⊢ F^{-1} [\{w\}] \subseteq dom F$
28	27 5	sseqtrid	$⊢ F : On \underset{onto}{⟶} V \to F^{-1} [\{w\}] \subseteq On$
29	18 8	eleqtrrid	$⊢ F : On \underset{onto}{⟶} V \to w \in ran F$
30		inisegn0	$⊢ w \in ran F \leftrightarrow F^{-1} [\{w\}] \neq \emptyset$
31	29 30	sylib	$⊢ F : On \underset{onto}{⟶} V \to F^{-1} [\{w\}] \neq \emptyset$
32		onint	$⊢ (F^{-1} [\{w\}] \subseteq On \land F^{-1} [\{w\}] \neq \emptyset) \to ⋂ F^{-1} [\{w\}] \in F^{-1} [\{w\}]$
33	28 31 32	syl2anc	$⊢ F : On \underset{onto}{⟶} V \to ⋂ F^{-1} [\{w\}] \in F^{-1} [\{w\}]$
34	26 33	eqeltrd	$⊢ F : On \underset{onto}{⟶} V \to H (w) \in F^{-1} [\{w\}]$
35		eleq1	$⊢ H (v) = H (w) \to (H (v) \in F^{-1} [\{w\}] \leftrightarrow H (w) \in F^{-1} [\{w\}])$
36	34 35	syl5ibrcom	$⊢ F : On \underset{onto}{⟶} V \to (H (v) = H (w) \to H (v) \in F^{-1} [\{w\}])$
37		vex	$⊢ v \in V$
38	37	a1i	$⊢ F : On \underset{onto}{⟶} V \to v \in V$
39	13	adantr	$⊢ (F : On \underset{onto}{⟶} V \land z = v) \to ⋂ F^{-1} [\{z\}] \in On$
40		sneq	$⊢ z = v \to \{z\} = \{v\}$
41	40	imaeq2d	$⊢ z = v \to F^{-1} [\{z\}] = F^{-1} [\{v\}]$
42	41	inteqd	$⊢ z = v \to ⋂ F^{-1} [\{z\}] = ⋂ F^{-1} [\{v\}]$
43	42	adantl	$⊢ (F : On \underset{onto}{⟶} V \land z = v) \to ⋂ F^{-1} [\{z\}] = ⋂ F^{-1} [\{v\}]$
44	38 39 43	fvmptdv2	$⊢ F : On \underset{onto}{⟶} V \to (H = (z \in V ⟼ ⋂ F^{-1} [\{z\}]) \to H (v) = ⋂ F^{-1} [\{v\}])$
45	2 44	mpi	$⊢ F : On \underset{onto}{⟶} V \to H (v) = ⋂ F^{-1} [\{v\}]$
46		cnvimass	$⊢ F^{-1} [\{v\}] \subseteq dom F$
47	46 5	sseqtrid	$⊢ F : On \underset{onto}{⟶} V \to F^{-1} [\{v\}] \subseteq On$
48	37 8	eleqtrrid	$⊢ F : On \underset{onto}{⟶} V \to v \in ran F$
49		inisegn0	$⊢ v \in ran F \leftrightarrow F^{-1} [\{v\}] \neq \emptyset$
50	48 49	sylib	$⊢ F : On \underset{onto}{⟶} V \to F^{-1} [\{v\}] \neq \emptyset$
51		onint	$⊢ (F^{-1} [\{v\}] \subseteq On \land F^{-1} [\{v\}] \neq \emptyset) \to ⋂ F^{-1} [\{v\}] \in F^{-1} [\{v\}]$
52	47 50 51	syl2anc	$⊢ F : On \underset{onto}{⟶} V \to ⋂ F^{-1} [\{v\}] \in F^{-1} [\{v\}]$
53	45 52	eqeltrd	$⊢ F : On \underset{onto}{⟶} V \to H (v) \in F^{-1} [\{v\}]$
54	36 53	jctild	$⊢ F : On \underset{onto}{⟶} V \to (H (v) = H (w) \to (H (v) \in F^{-1} [\{v\}] \land H (v) \in F^{-1} [\{w\}]))$
55	54	imp	$⊢ (F : On \underset{onto}{⟶} V \land H (v) = H (w)) \to (H (v) \in F^{-1} [\{v\}] \land H (v) \in F^{-1} [\{w\}])$
56		eleq1	$⊢ u = H (v) \to (u \in F^{-1} [\{v\}] \leftrightarrow H (v) \in F^{-1} [\{v\}])$
57		eleq1	$⊢ u = H (v) \to (u \in F^{-1} [\{w\}] \leftrightarrow H (v) \in F^{-1} [\{w\}])$
58	56 57	anbi12d	$⊢ u = H (v) \to ((u \in F^{-1} [\{v\}] \land u \in F^{-1} [\{w\}]) \leftrightarrow (H (v) \in F^{-1} [\{v\}] \land H (v) \in F^{-1} [\{w\}]))$
59	17 55 58	spcedv	$⊢ (F : On \underset{onto}{⟶} V \land H (v) = H (w)) \to \exists u (u \in F^{-1} [\{v\}] \land u \in F^{-1} [\{w\}])$
60	59	ex	$⊢ F : On \underset{onto}{⟶} V \to (H (v) = H (w) \to \exists u (u \in F^{-1} [\{v\}] \land u \in F^{-1} [\{w\}]))$
61		elinisegg	$⊢ (v \in V \land u \in V) \to (u \in F^{-1} [\{v\}] \leftrightarrow u F v)$
62	61	el2v	$⊢ u \in F^{-1} [\{v\}] \leftrightarrow u F v$
63		elinisegg	$⊢ (w \in V \land u \in V) \to (u \in F^{-1} [\{w\}] \leftrightarrow u F w)$
64	63	el2v	$⊢ u \in F^{-1} [\{w\}] \leftrightarrow u F w$
65	62 64	anbi12i	$⊢ (u \in F^{-1} [\{v\}] \land u \in F^{-1} [\{w\}]) \leftrightarrow (u F v \land u F w)$
66	65	exbii	$⊢ \exists u (u \in F^{-1} [\{v\}] \land u \in F^{-1} [\{w\}]) \leftrightarrow \exists u (u F v \land u F w)$
67	60 66	imbitrdi	$⊢ F : On \underset{onto}{⟶} V \to (H (v) = H (w) \to \exists u (u F v \land u F w))$
68		funeu	$⊢ (Fun F \land u F v) \to \exists! v u F v$
69	68	3adant3	$⊢ (Fun F \land u F v \land u F w) \to \exists! v u F v$
70		3simpc	$⊢ (Fun F \land u F v \land u F w) \to (u F v \land u F w)$
71		breq2	$⊢ v = w \to (u F v \leftrightarrow u F w)$
72	71	eu4	$⊢ \exists! v u F v \leftrightarrow (\exists v u F v \land \forall v \forall w ((u F v \land u F w) \to v = w))$
73	72	simprbi	$⊢ \exists! v u F v \to \forall v \forall w ((u F v \land u F w) \to v = w)$
74	73	19.21bbi	$⊢ \exists! v u F v \to ((u F v \land u F w) \to v = w)$
75	69 70 74	sylc	$⊢ (Fun F \land u F v \land u F w) \to v = w$
76	75	3expib	$⊢ Fun F \to ((u F v \land u F w) \to v = w)$
77	76	exlimdv	$⊢ Fun F \to (\exists u (u F v \land u F w) \to v = w)$
78	16 67 77	sylsyld	$⊢ F : On \underset{onto}{⟶} V \to (H (v) = H (w) \to v = w)$
79	78	ralrimivw	$⊢ F : On \underset{onto}{⟶} V \to \forall w \in V (H (v) = H (w) \to v = w)$
80	79	ralrimivw	$⊢ F : On \underset{onto}{⟶} V \to \forall v \in V \forall w \in V (H (v) = H (w) \to v = w)$
81		dff13	$⊢ H : V \underset{1-1}{⟶} On \leftrightarrow (H : V ⟶ On \land \forall v \in V \forall w \in V (H (v) = H (w) \to v = w))$
82	15 80 81	sylanbrc	$⊢ F : On \underset{onto}{⟶} V \to H : V \underset{1-1}{⟶} On$
83	1	vonf1wev	$⊢ H : V \underset{1-1}{⟶} On \to R We V$
84	82 83	syl	$⊢ F : On \underset{onto}{⟶} V \to R We V$

Metamath Proof Explorer

Theorem onvfowev

Proof