Theorem 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	⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐻 ‘ 𝑥 ) ∈ ( 𝐻 ‘ 𝑦 ) }
	onvfowev.2	⊢ 𝐻 = ( 𝑧 ∈ V ↦ ∩ ( ◡ 𝐹 “ { 𝑧 } ) )
Assertion	onvfowev	⊢ ( 𝐹 : On –onto→ V → 𝑅 We V )

Proof

Step	Hyp	Ref	Expression
1		onvfowev.1	⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐻 ‘ 𝑥 ) ∈ ( 𝐻 ‘ 𝑦 ) }
2		onvfowev.2	⊢ 𝐻 = ( 𝑧 ∈ V ↦ ∩ ( ◡ 𝐹 “ { 𝑧 } ) )
3		cnvimass	⊢ ( ◡ 𝐹 “ { 𝑧 } ) ⊆ dom 𝐹
4		fofn	⊢ ( 𝐹 : On –onto→ V → 𝐹 Fn On )
5	4	fndmd	⊢ ( 𝐹 : On –onto→ V → dom 𝐹 = On )
6	3 5	sseqtrid	⊢ ( 𝐹 : On –onto→ V → ( ◡ 𝐹 “ { 𝑧 } ) ⊆ On )
7		vex	⊢ 𝑧 ∈ V
8		forn	⊢ ( 𝐹 : On –onto→ V → ran 𝐹 = V )
9	7 8	eleqtrrid	⊢ ( 𝐹 : On –onto→ V → 𝑧 ∈ ran 𝐹 )
10		inisegn0	⊢ ( 𝑧 ∈ ran 𝐹 ↔ ( ◡ 𝐹 “ { 𝑧 } ) ≠ ∅ )
11	9 10	sylib	⊢ ( 𝐹 : On –onto→ V → ( ◡ 𝐹 “ { 𝑧 } ) ≠ ∅ )
12		oninton	⊢ ( ( ( ◡ 𝐹 “ { 𝑧 } ) ⊆ On ∧ ( ◡ 𝐹 “ { 𝑧 } ) ≠ ∅ ) → ∩ ( ◡ 𝐹 “ { 𝑧 } ) ∈ On )
13	6 11 12	syl2anc	⊢ ( 𝐹 : On –onto→ V → ∩ ( ◡ 𝐹 “ { 𝑧 } ) ∈ On )
14	13	adantr	⊢ ( ( 𝐹 : On –onto→ V ∧ 𝑧 ∈ V ) → ∩ ( ◡ 𝐹 “ { 𝑧 } ) ∈ On )
15	14 2	fmptd	⊢ ( 𝐹 : On –onto→ V → 𝐻 : V ⟶ On )
16		fofun	⊢ ( 𝐹 : On –onto→ V → Fun 𝐹 )
17		fvexd	⊢ ( ( 𝐹 : On –onto→ V ∧ ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑤 ) ) → ( 𝐻 ‘ 𝑣 ) ∈ V )
18		vex	⊢ 𝑤 ∈ V
19	18	a1i	⊢ ( 𝐹 : On –onto→ V → 𝑤 ∈ V )
20	13	adantr	⊢ ( ( 𝐹 : On –onto→ V ∧ 𝑧 = 𝑤 ) → ∩ ( ◡ 𝐹 “ { 𝑧 } ) ∈ On )
21		sneq	⊢ ( 𝑧 = 𝑤 → { 𝑧 } = { 𝑤 } )
22	21	imaeq2d	⊢ ( 𝑧 = 𝑤 → ( ◡ 𝐹 “ { 𝑧 } ) = ( ◡ 𝐹 “ { 𝑤 } ) )
23	22	inteqd	⊢ ( 𝑧 = 𝑤 → ∩ ( ◡ 𝐹 “ { 𝑧 } ) = ∩ ( ◡ 𝐹 “ { 𝑤 } ) )
24	23	adantl	⊢ ( ( 𝐹 : On –onto→ V ∧ 𝑧 = 𝑤 ) → ∩ ( ◡ 𝐹 “ { 𝑧 } ) = ∩ ( ◡ 𝐹 “ { 𝑤 } ) )
25	19 20 24	fvmptdv2	⊢ ( 𝐹 : On –onto→ V → ( 𝐻 = ( 𝑧 ∈ V ↦ ∩ ( ◡ 𝐹 “ { 𝑧 } ) ) → ( 𝐻 ‘ 𝑤 ) = ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) )
26	2 25	mpi	⊢ ( 𝐹 : On –onto→ V → ( 𝐻 ‘ 𝑤 ) = ∩ ( ◡ 𝐹 “ { 𝑤 } ) )
27		cnvimass	⊢ ( ◡ 𝐹 “ { 𝑤 } ) ⊆ dom 𝐹
28	27 5	sseqtrid	⊢ ( 𝐹 : On –onto→ V → ( ◡ 𝐹 “ { 𝑤 } ) ⊆ On )
29	18 8	eleqtrrid	⊢ ( 𝐹 : On –onto→ V → 𝑤 ∈ ran 𝐹 )
30		inisegn0	⊢ ( 𝑤 ∈ ran 𝐹 ↔ ( ◡ 𝐹 “ { 𝑤 } ) ≠ ∅ )
31	29 30	sylib	⊢ ( 𝐹 : On –onto→ V → ( ◡ 𝐹 “ { 𝑤 } ) ≠ ∅ )
32		onint	⊢ ( ( ( ◡ 𝐹 “ { 𝑤 } ) ⊆ On ∧ ( ◡ 𝐹 “ { 𝑤 } ) ≠ ∅ ) → ∩ ( ◡ 𝐹 “ { 𝑤 } ) ∈ ( ◡ 𝐹 “ { 𝑤 } ) )
33	28 31 32	syl2anc	⊢ ( 𝐹 : On –onto→ V → ∩ ( ◡ 𝐹 “ { 𝑤 } ) ∈ ( ◡ 𝐹 “ { 𝑤 } ) )
34	26 33	eqeltrd	⊢ ( 𝐹 : On –onto→ V → ( 𝐻 ‘ 𝑤 ) ∈ ( ◡ 𝐹 “ { 𝑤 } ) )
35		eleq1	⊢ ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑤 ) → ( ( 𝐻 ‘ 𝑣 ) ∈ ( ◡ 𝐹 “ { 𝑤 } ) ↔ ( 𝐻 ‘ 𝑤 ) ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) )
36	34 35	syl5ibrcom	⊢ ( 𝐹 : On –onto→ V → ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑤 ) → ( 𝐻 ‘ 𝑣 ) ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) )
37		vex	⊢ 𝑣 ∈ V
38	37	a1i	⊢ ( 𝐹 : On –onto→ V → 𝑣 ∈ V )
39	13	adantr	⊢ ( ( 𝐹 : On –onto→ V ∧ 𝑧 = 𝑣 ) → ∩ ( ◡ 𝐹 “ { 𝑧 } ) ∈ On )
40		sneq	⊢ ( 𝑧 = 𝑣 → { 𝑧 } = { 𝑣 } )
41	40	imaeq2d	⊢ ( 𝑧 = 𝑣 → ( ◡ 𝐹 “ { 𝑧 } ) = ( ◡ 𝐹 “ { 𝑣 } ) )
42	41	inteqd	⊢ ( 𝑧 = 𝑣 → ∩ ( ◡ 𝐹 “ { 𝑧 } ) = ∩ ( ◡ 𝐹 “ { 𝑣 } ) )
43	42	adantl	⊢ ( ( 𝐹 : On –onto→ V ∧ 𝑧 = 𝑣 ) → ∩ ( ◡ 𝐹 “ { 𝑧 } ) = ∩ ( ◡ 𝐹 “ { 𝑣 } ) )
44	38 39 43	fvmptdv2	⊢ ( 𝐹 : On –onto→ V → ( 𝐻 = ( 𝑧 ∈ V ↦ ∩ ( ◡ 𝐹 “ { 𝑧 } ) ) → ( 𝐻 ‘ 𝑣 ) = ∩ ( ◡ 𝐹 “ { 𝑣 } ) ) )
45	2 44	mpi	⊢ ( 𝐹 : On –onto→ V → ( 𝐻 ‘ 𝑣 ) = ∩ ( ◡ 𝐹 “ { 𝑣 } ) )
46		cnvimass	⊢ ( ◡ 𝐹 “ { 𝑣 } ) ⊆ dom 𝐹
47	46 5	sseqtrid	⊢ ( 𝐹 : On –onto→ V → ( ◡ 𝐹 “ { 𝑣 } ) ⊆ On )
48	37 8	eleqtrrid	⊢ ( 𝐹 : On –onto→ V → 𝑣 ∈ ran 𝐹 )
49		inisegn0	⊢ ( 𝑣 ∈ ran 𝐹 ↔ ( ◡ 𝐹 “ { 𝑣 } ) ≠ ∅ )
50	48 49	sylib	⊢ ( 𝐹 : On –onto→ V → ( ◡ 𝐹 “ { 𝑣 } ) ≠ ∅ )
51		onint	⊢ ( ( ( ◡ 𝐹 “ { 𝑣 } ) ⊆ On ∧ ( ◡ 𝐹 “ { 𝑣 } ) ≠ ∅ ) → ∩ ( ◡ 𝐹 “ { 𝑣 } ) ∈ ( ◡ 𝐹 “ { 𝑣 } ) )
52	47 50 51	syl2anc	⊢ ( 𝐹 : On –onto→ V → ∩ ( ◡ 𝐹 “ { 𝑣 } ) ∈ ( ◡ 𝐹 “ { 𝑣 } ) )
53	45 52	eqeltrd	⊢ ( 𝐹 : On –onto→ V → ( 𝐻 ‘ 𝑣 ) ∈ ( ◡ 𝐹 “ { 𝑣 } ) )
54	36 53	jctild	⊢ ( 𝐹 : On –onto→ V → ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑤 ) → ( ( 𝐻 ‘ 𝑣 ) ∈ ( ◡ 𝐹 “ { 𝑣 } ) ∧ ( 𝐻 ‘ 𝑣 ) ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) )
55	54	imp	⊢ ( ( 𝐹 : On –onto→ V ∧ ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑤 ) ) → ( ( 𝐻 ‘ 𝑣 ) ∈ ( ◡ 𝐹 “ { 𝑣 } ) ∧ ( 𝐻 ‘ 𝑣 ) ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) )
56		eleq1	⊢ ( 𝑢 = ( 𝐻 ‘ 𝑣 ) → ( 𝑢 ∈ ( ◡ 𝐹 “ { 𝑣 } ) ↔ ( 𝐻 ‘ 𝑣 ) ∈ ( ◡ 𝐹 “ { 𝑣 } ) ) )
57		eleq1	⊢ ( 𝑢 = ( 𝐻 ‘ 𝑣 ) → ( 𝑢 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ↔ ( 𝐻 ‘ 𝑣 ) ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) )
58	56 57	anbi12d	⊢ ( 𝑢 = ( 𝐻 ‘ 𝑣 ) → ( ( 𝑢 ∈ ( ◡ 𝐹 “ { 𝑣 } ) ∧ 𝑢 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ↔ ( ( 𝐻 ‘ 𝑣 ) ∈ ( ◡ 𝐹 “ { 𝑣 } ) ∧ ( 𝐻 ‘ 𝑣 ) ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) )
59	17 55 58	spcedv	⊢ ( ( 𝐹 : On –onto→ V ∧ ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑤 ) ) → ∃ 𝑢 ( 𝑢 ∈ ( ◡ 𝐹 “ { 𝑣 } ) ∧ 𝑢 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) )
60	59	ex	⊢ ( 𝐹 : On –onto→ V → ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑤 ) → ∃ 𝑢 ( 𝑢 ∈ ( ◡ 𝐹 “ { 𝑣 } ) ∧ 𝑢 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) )
61		elinisegg	⊢ ( ( 𝑣 ∈ V ∧ 𝑢 ∈ V ) → ( 𝑢 ∈ ( ◡ 𝐹 “ { 𝑣 } ) ↔ 𝑢 𝐹 𝑣 ) )
62	61	el2v	⊢ ( 𝑢 ∈ ( ◡ 𝐹 “ { 𝑣 } ) ↔ 𝑢 𝐹 𝑣 )
63		elinisegg	⊢ ( ( 𝑤 ∈ V ∧ 𝑢 ∈ V ) → ( 𝑢 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ↔ 𝑢 𝐹 𝑤 ) )
64	63	el2v	⊢ ( 𝑢 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ↔ 𝑢 𝐹 𝑤 )
65	62 64	anbi12i	⊢ ( ( 𝑢 ∈ ( ◡ 𝐹 “ { 𝑣 } ) ∧ 𝑢 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ↔ ( 𝑢 𝐹 𝑣 ∧ 𝑢 𝐹 𝑤 ) )
66	65	exbii	⊢ ( ∃ 𝑢 ( 𝑢 ∈ ( ◡ 𝐹 “ { 𝑣 } ) ∧ 𝑢 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ↔ ∃ 𝑢 ( 𝑢 𝐹 𝑣 ∧ 𝑢 𝐹 𝑤 ) )
67	60 66	imbitrdi	⊢ ( 𝐹 : On –onto→ V → ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑤 ) → ∃ 𝑢 ( 𝑢 𝐹 𝑣 ∧ 𝑢 𝐹 𝑤 ) ) )
68		funeu	⊢ ( ( Fun 𝐹 ∧ 𝑢 𝐹 𝑣 ) → ∃! 𝑣 𝑢 𝐹 𝑣 )
69	68	3adant3	⊢ ( ( Fun 𝐹 ∧ 𝑢 𝐹 𝑣 ∧ 𝑢 𝐹 𝑤 ) → ∃! 𝑣 𝑢 𝐹 𝑣 )
70		3simpc	⊢ ( ( Fun 𝐹 ∧ 𝑢 𝐹 𝑣 ∧ 𝑢 𝐹 𝑤 ) → ( 𝑢 𝐹 𝑣 ∧ 𝑢 𝐹 𝑤 ) )
71		breq2	⊢ ( 𝑣 = 𝑤 → ( 𝑢 𝐹 𝑣 ↔ 𝑢 𝐹 𝑤 ) )
72	71	eu4	⊢ ( ∃! 𝑣 𝑢 𝐹 𝑣 ↔ ( ∃ 𝑣 𝑢 𝐹 𝑣 ∧ ∀ 𝑣 ∀ 𝑤 ( ( 𝑢 𝐹 𝑣 ∧ 𝑢 𝐹 𝑤 ) → 𝑣 = 𝑤 ) ) )
73	72	simprbi	⊢ ( ∃! 𝑣 𝑢 𝐹 𝑣 → ∀ 𝑣 ∀ 𝑤 ( ( 𝑢 𝐹 𝑣 ∧ 𝑢 𝐹 𝑤 ) → 𝑣 = 𝑤 ) )
74	73	19.21bbi	⊢ ( ∃! 𝑣 𝑢 𝐹 𝑣 → ( ( 𝑢 𝐹 𝑣 ∧ 𝑢 𝐹 𝑤 ) → 𝑣 = 𝑤 ) )
75	69 70 74	sylc	⊢ ( ( Fun 𝐹 ∧ 𝑢 𝐹 𝑣 ∧ 𝑢 𝐹 𝑤 ) → 𝑣 = 𝑤 )
76	75	3expib	⊢ ( Fun 𝐹 → ( ( 𝑢 𝐹 𝑣 ∧ 𝑢 𝐹 𝑤 ) → 𝑣 = 𝑤 ) )
77	76	exlimdv	⊢ ( Fun 𝐹 → ( ∃ 𝑢 ( 𝑢 𝐹 𝑣 ∧ 𝑢 𝐹 𝑤 ) → 𝑣 = 𝑤 ) )
78	16 67 77	sylsyld	⊢ ( 𝐹 : On –onto→ V → ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑤 ) → 𝑣 = 𝑤 ) )
79	78	ralrimivw	⊢ ( 𝐹 : On –onto→ V → ∀ 𝑤 ∈ V ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑤 ) → 𝑣 = 𝑤 ) )
80	79	ralrimivw	⊢ ( 𝐹 : On –onto→ V → ∀ 𝑣 ∈ V ∀ 𝑤 ∈ V ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑤 ) → 𝑣 = 𝑤 ) )
81		dff13	⊢ ( 𝐻 : V –1-1→ On ↔ ( 𝐻 : V ⟶ On ∧ ∀ 𝑣 ∈ V ∀ 𝑤 ∈ V ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑤 ) → 𝑣 = 𝑤 ) ) )
82	15 80 81	sylanbrc	⊢ ( 𝐹 : On –onto→ V → 𝐻 : V –1-1→ On )
83	1	vonf1wev	⊢ ( 𝐻 : V –1-1→ On → 𝑅 We V )
84	82 83	syl	⊢ ( 𝐹 : On –onto→ V → 𝑅 We V )