Theorem vonf1wev 35570

Description: If 𝐹 maps the universe one-to-one into the ordinals, then 𝑅 well-orders the universe. This is the ZFC version of (6 → 3) which is used in place of (7 → 3) in https://tinyurl.com/hamkins-gblac. Note that in NBG set theory the antecedent would be something like ∀𝑋∃𝐹𝐹:𝑋–1-1→On, but since we cannot quantify over classes, we instead consider only the case 𝑋 = V which is sufficient for this proof. (Contributed by BTernaryTau, 11-Jun-2026.)

Hypothesis

Ref	Expression
vonf1wev.1	⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝐹‘𝑥) ∈ (𝐹‘𝑦)}

Assertion

Ref	Expression
vonf1wev	⊢ (𝐹:V–1-1→On → 𝑅 We V)

Distinct variable group:   𝑥,𝐹,𝑦

Allowed substitution hints:   𝑅(𝑥,𝑦)

Proof of Theorem vonf1wev

Dummy variables 𝑤 𝑧 𝑡 𝑢 𝑣 𝑠 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		f1f 6776	. . . . . . . 8 ⊢ (𝐹:V–1-1→On → 𝐹:V⟶On)
2	1	fimassd 6729	. . . . . . 7 ⊢ (𝐹:V–1-1→On → (𝐹 “ 𝑡) ⊆ On)
3		f1dm 6782	. . . . . . . . . . . 12 ⊢ (𝐹:V–1-1→On → dom 𝐹 = V)
4	3	ineq1d 4173	. . . . . . . . . . 11 ⊢ (𝐹:V–1-1→On → (dom 𝐹 ∩ 𝑡) = (V ∩ 𝑡))
5	4	neeq1d 3017	. . . . . . . . . 10 ⊢ (𝐹:V–1-1→On → ((dom 𝐹 ∩ 𝑡) ≠ ∅ ↔ (V ∩ 𝑡) ≠ ∅))
6		inv1 4356	. . . . . . . . . . . 12 ⊢ (𝑡 ∩ V) = 𝑡
7	6	ineqcomi 4165	. . . . . . . . . . 11 ⊢ (V ∩ 𝑡) = 𝑡
8	7	neeq1i 3022	. . . . . . . . . 10 ⊢ ((V ∩ 𝑡) ≠ ∅ ↔ 𝑡 ≠ ∅)
9	5, 8	bitr2di 291	. . . . . . . . 9 ⊢ (𝐹:V–1-1→On → (𝑡 ≠ ∅ ↔ (dom 𝐹 ∩ 𝑡) ≠ ∅))
10	9	biimpa 481	. . . . . . . 8 ⊢ ((𝐹:V–1-1→On ∧ 𝑡 ≠ ∅) → (dom 𝐹 ∩ 𝑡) ≠ ∅)
11	10	imadisjlnd 6085	. . . . . . 7 ⊢ ((𝐹:V–1-1→On ∧ 𝑡 ≠ ∅) → (𝐹 “ 𝑡) ≠ ∅)
12		onssmin 7792	. . . . . . 7 ⊢ (((𝐹 “ 𝑡) ⊆ On ∧ (𝐹 “ 𝑡) ≠ ∅) → ∃𝑟 ∈ (𝐹 “ 𝑡)∀𝑠 ∈ (𝐹 “ 𝑡)𝑟 ⊆ 𝑠)
13	2, 11, 12	syl2an2r 697	. . . . . 6 ⊢ ((𝐹:V–1-1→On ∧ 𝑡 ≠ ∅) → ∃𝑟 ∈ (𝐹 “ 𝑡)∀𝑠 ∈ (𝐹 “ 𝑡)𝑟 ⊆ 𝑠)
14	13	ex 417	. . . . 5 ⊢ (𝐹:V–1-1→On → (𝑡 ≠ ∅ → ∃𝑟 ∈ (𝐹 “ 𝑡)∀𝑠 ∈ (𝐹 “ 𝑡)𝑟 ⊆ 𝑠))
15		vex 3459	. . . . . . . . . . . 12 ⊢ 𝑣 ∈ V
16		vex 3459	. . . . . . . . . . . 12 ⊢ 𝑢 ∈ V
17		fveq2 6883	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑣 → (𝐹‘𝑥) = (𝐹‘𝑣))
18	17	eleq1d 2848	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑣 → ((𝐹‘𝑥) ∈ (𝐹‘𝑦) ↔ (𝐹‘𝑣) ∈ (𝐹‘𝑦)))
19		fveq2 6883	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑢 → (𝐹‘𝑦) = (𝐹‘𝑢))
20	19	eleq2d 2849	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑢 → ((𝐹‘𝑣) ∈ (𝐹‘𝑦) ↔ (𝐹‘𝑣) ∈ (𝐹‘𝑢)))
21		vonf1wev.1	. . . . . . . . . . . 12 ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝐹‘𝑥) ∈ (𝐹‘𝑦)}
22	15, 16, 18, 20, 21	brab 5530	. . . . . . . . . . 11 ⊢ (𝑣𝑅𝑢 ↔ (𝐹‘𝑣) ∈ (𝐹‘𝑢))
23	22	notbii 323	. . . . . . . . . 10 ⊢ (¬ 𝑣𝑅𝑢 ↔ ¬ (𝐹‘𝑣) ∈ (𝐹‘𝑢))
24	1	ffvelcdmda 7081	. . . . . . . . . . . 12 ⊢ ((𝐹:V–1-1→On ∧ 𝑢 ∈ V) → (𝐹‘𝑢) ∈ On)
25	24	elvd 3461	. . . . . . . . . . 11 ⊢ (𝐹:V–1-1→On → (𝐹‘𝑢) ∈ On)
26	1	ffvelcdmda 7081	. . . . . . . . . . . 12 ⊢ ((𝐹:V–1-1→On ∧ 𝑣 ∈ V) → (𝐹‘𝑣) ∈ On)
27	26	elvd 3461	. . . . . . . . . . 11 ⊢ (𝐹:V–1-1→On → (𝐹‘𝑣) ∈ On)
28		ontri1 6397	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑢) ∈ On ∧ (𝐹‘𝑣) ∈ On) → ((𝐹‘𝑢) ⊆ (𝐹‘𝑣) ↔ ¬ (𝐹‘𝑣) ∈ (𝐹‘𝑢)))
29	25, 27, 28	syl2anc 595	. . . . . . . . . 10 ⊢ (𝐹:V–1-1→On → ((𝐹‘𝑢) ⊆ (𝐹‘𝑣) ↔ ¬ (𝐹‘𝑣) ∈ (𝐹‘𝑢)))
30	23, 29	bitr4id 293	. . . . . . . . 9 ⊢ (𝐹:V–1-1→On → (¬ 𝑣𝑅𝑢 ↔ (𝐹‘𝑢) ⊆ (𝐹‘𝑣)))
31	30	ralbidv 3188	. . . . . . . 8 ⊢ (𝐹:V–1-1→On → (∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢 ↔ ∀𝑣 ∈ 𝑡 (𝐹‘𝑢) ⊆ (𝐹‘𝑣)))
32		f1fn 6777	. . . . . . . . 9 ⊢ (𝐹:V–1-1→On → 𝐹 Fn V)
33		ssv 3962	. . . . . . . . 9 ⊢ 𝑡 ⊆ V
34		sseq2 3964	. . . . . . . . . 10 ⊢ (𝑠 = (𝐹‘𝑣) → ((𝐹‘𝑢) ⊆ 𝑠 ↔ (𝐹‘𝑢) ⊆ (𝐹‘𝑣)))
35	34	ralima 7237	. . . . . . . . 9 ⊢ ((𝐹 Fn V ∧ 𝑡 ⊆ V) → (∀𝑠 ∈ (𝐹 “ 𝑡)(𝐹‘𝑢) ⊆ 𝑠 ↔ ∀𝑣 ∈ 𝑡 (𝐹‘𝑢) ⊆ (𝐹‘𝑣)))
36	32, 33, 35	sylancl 597	. . . . . . . 8 ⊢ (𝐹:V–1-1→On → (∀𝑠 ∈ (𝐹 “ 𝑡)(𝐹‘𝑢) ⊆ 𝑠 ↔ ∀𝑣 ∈ 𝑡 (𝐹‘𝑢) ⊆ (𝐹‘𝑣)))
37	31, 36	bitr4d 285	. . . . . . 7 ⊢ (𝐹:V–1-1→On → (∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢 ↔ ∀𝑠 ∈ (𝐹 “ 𝑡)(𝐹‘𝑢) ⊆ 𝑠))
38	37	rexbidv 3189	. . . . . 6 ⊢ (𝐹:V–1-1→On → (∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢 ↔ ∃𝑢 ∈ 𝑡 ∀𝑠 ∈ (𝐹 “ 𝑡)(𝐹‘𝑢) ⊆ 𝑠))
39		sseq1 3963	. . . . . . . . 9 ⊢ (𝑟 = (𝐹‘𝑢) → (𝑟 ⊆ 𝑠 ↔ (𝐹‘𝑢) ⊆ 𝑠))
40	39	ralbidv 3188	. . . . . . . 8 ⊢ (𝑟 = (𝐹‘𝑢) → (∀𝑠 ∈ (𝐹 “ 𝑡)𝑟 ⊆ 𝑠 ↔ ∀𝑠 ∈ (𝐹 “ 𝑡)(𝐹‘𝑢) ⊆ 𝑠))
41	40	rexima 7238	. . . . . . 7 ⊢ ((𝐹 Fn V ∧ 𝑡 ⊆ V) → (∃𝑟 ∈ (𝐹 “ 𝑡)∀𝑠 ∈ (𝐹 “ 𝑡)𝑟 ⊆ 𝑠 ↔ ∃𝑢 ∈ 𝑡 ∀𝑠 ∈ (𝐹 “ 𝑡)(𝐹‘𝑢) ⊆ 𝑠))
42	32, 33, 41	sylancl 597	. . . . . 6 ⊢ (𝐹:V–1-1→On → (∃𝑟 ∈ (𝐹 “ 𝑡)∀𝑠 ∈ (𝐹 “ 𝑡)𝑟 ⊆ 𝑠 ↔ ∃𝑢 ∈ 𝑡 ∀𝑠 ∈ (𝐹 “ 𝑡)(𝐹‘𝑢) ⊆ 𝑠))
43	38, 42	bitr4d 285	. . . . 5 ⊢ (𝐹:V–1-1→On → (∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢 ↔ ∃𝑟 ∈ (𝐹 “ 𝑡)∀𝑠 ∈ (𝐹 “ 𝑡)𝑟 ⊆ 𝑠))
44	14, 43	sylibrd 262	. . . 4 ⊢ (𝐹:V–1-1→On → (𝑡 ≠ ∅ → ∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢))
45	44	alrimiv 1957	. . 3 ⊢ (𝐹:V–1-1→On → ∀𝑡(𝑡 ≠ ∅ → ∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢))
46		df-fr 5616	. . . 4 ⊢ (𝑅 Fr V ↔ ∀𝑡((𝑡 ⊆ V ∧ 𝑡 ≠ ∅) → ∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢))
47	33	biantrur 539	. . . . . 6 ⊢ (𝑡 ≠ ∅ ↔ (𝑡 ⊆ V ∧ 𝑡 ≠ ∅))
48	47	imbi1i 352	. . . . 5 ⊢ ((𝑡 ≠ ∅ → ∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢) ↔ ((𝑡 ⊆ V ∧ 𝑡 ≠ ∅) → ∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢))
49	48	albii 1849	. . . 4 ⊢ (∀𝑡(𝑡 ≠ ∅ → ∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢) ↔ ∀𝑡((𝑡 ⊆ V ∧ 𝑡 ≠ ∅) → ∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢))
50	46, 49	bitr4i 281	. . 3 ⊢ (𝑅 Fr V ↔ ∀𝑡(𝑡 ≠ ∅ → ∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢))
51	45, 50	sylibr 237	. 2 ⊢ (𝐹:V–1-1→On → 𝑅 Fr V)
52	1	ffvelcdmda 7081	. . . . . . . 8 ⊢ ((𝐹:V–1-1→On ∧ 𝑤 ∈ V) → (𝐹‘𝑤) ∈ On)
53	52	elvd 3461	. . . . . . 7 ⊢ (𝐹:V–1-1→On → (𝐹‘𝑤) ∈ On)
54	1	ffvelcdmda 7081	. . . . . . . 8 ⊢ ((𝐹:V–1-1→On ∧ 𝑧 ∈ V) → (𝐹‘𝑧) ∈ On)
55	54	elvd 3461	. . . . . . 7 ⊢ (𝐹:V–1-1→On → (𝐹‘𝑧) ∈ On)
56		oneltri 6406	. . . . . . 7 ⊢ (((𝐹‘𝑤) ∈ On ∧ (𝐹‘𝑧) ∈ On) → ((𝐹‘𝑤) ∈ (𝐹‘𝑧) ∨ (𝐹‘𝑧) ∈ (𝐹‘𝑤) ∨ (𝐹‘𝑤) = (𝐹‘𝑧)))
57	53, 55, 56	syl2anc 595	. . . . . 6 ⊢ (𝐹:V–1-1→On → ((𝐹‘𝑤) ∈ (𝐹‘𝑧) ∨ (𝐹‘𝑧) ∈ (𝐹‘𝑤) ∨ (𝐹‘𝑤) = (𝐹‘𝑧)))
58		3orcomb 1110	. . . . . 6 ⊢ (((𝐹‘𝑤) ∈ (𝐹‘𝑧) ∨ (𝐹‘𝑧) ∈ (𝐹‘𝑤) ∨ (𝐹‘𝑤) = (𝐹‘𝑧)) ↔ ((𝐹‘𝑤) ∈ (𝐹‘𝑧) ∨ (𝐹‘𝑤) = (𝐹‘𝑧) ∨ (𝐹‘𝑧) ∈ (𝐹‘𝑤)))
59	57, 58	sylib 221	. . . . 5 ⊢ (𝐹:V–1-1→On → ((𝐹‘𝑤) ∈ (𝐹‘𝑧) ∨ (𝐹‘𝑤) = (𝐹‘𝑧) ∨ (𝐹‘𝑧) ∈ (𝐹‘𝑤)))
60		vex 3459	. . . . . . . . 9 ⊢ 𝑤 ∈ V
61		vex 3459	. . . . . . . . 9 ⊢ 𝑧 ∈ V
62		fveq2 6883	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → (𝐹‘𝑥) = (𝐹‘𝑤))
63	62	eleq1d 2848	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → ((𝐹‘𝑥) ∈ (𝐹‘𝑦) ↔ (𝐹‘𝑤) ∈ (𝐹‘𝑦)))
64		fveq2 6883	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧))
65	64	eleq2d 2849	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ((𝐹‘𝑤) ∈ (𝐹‘𝑦) ↔ (𝐹‘𝑤) ∈ (𝐹‘𝑧)))
66	60, 61, 63, 65, 21	brab 5530	. . . . . . . 8 ⊢ (𝑤𝑅𝑧 ↔ (𝐹‘𝑤) ∈ (𝐹‘𝑧))
67	66	biimpri 231	. . . . . . 7 ⊢ ((𝐹‘𝑤) ∈ (𝐹‘𝑧) → 𝑤𝑅𝑧)
68	67	a1i 11	. . . . . 6 ⊢ (𝐹:V–1-1→On → ((𝐹‘𝑤) ∈ (𝐹‘𝑧) → 𝑤𝑅𝑧))
69		f1veqaeq 7256	. . . . . . 7 ⊢ ((𝐹:V–1-1→On ∧ (𝑤 ∈ V ∧ 𝑧 ∈ V)) → ((𝐹‘𝑤) = (𝐹‘𝑧) → 𝑤 = 𝑧))
70	60, 61, 69	mpanr12 717	. . . . . 6 ⊢ (𝐹:V–1-1→On → ((𝐹‘𝑤) = (𝐹‘𝑧) → 𝑤 = 𝑧))
71		fveq2 6883	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
72	71	eleq1d 2848	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) ∈ (𝐹‘𝑦) ↔ (𝐹‘𝑧) ∈ (𝐹‘𝑦)))
73		fveq2 6883	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → (𝐹‘𝑦) = (𝐹‘𝑤))
74	73	eleq2d 2849	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → ((𝐹‘𝑧) ∈ (𝐹‘𝑦) ↔ (𝐹‘𝑧) ∈ (𝐹‘𝑤)))
75	61, 60, 72, 74, 21	brab 5530	. . . . . . . 8 ⊢ (𝑧𝑅𝑤 ↔ (𝐹‘𝑧) ∈ (𝐹‘𝑤))
76	75	biimpri 231	. . . . . . 7 ⊢ ((𝐹‘𝑧) ∈ (𝐹‘𝑤) → 𝑧𝑅𝑤)
77	76	a1i 11	. . . . . 6 ⊢ (𝐹:V–1-1→On → ((𝐹‘𝑧) ∈ (𝐹‘𝑤) → 𝑧𝑅𝑤))
78	68, 70, 77	3orim123d 1472	. . . . 5 ⊢ (𝐹:V–1-1→On → (((𝐹‘𝑤) ∈ (𝐹‘𝑧) ∨ (𝐹‘𝑤) = (𝐹‘𝑧) ∨ (𝐹‘𝑧) ∈ (𝐹‘𝑤)) → (𝑤𝑅𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧𝑅𝑤)))
79	59, 78	mpd 16	. . . 4 ⊢ (𝐹:V–1-1→On → (𝑤𝑅𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧𝑅𝑤))
80	79	ralrimivw 3161	. . 3 ⊢ (𝐹:V–1-1→On → ∀𝑧 ∈ V (𝑤𝑅𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧𝑅𝑤))
81	80	ralrimivw 3161	. 2 ⊢ (𝐹:V–1-1→On → ∀𝑤 ∈ V ∀𝑧 ∈ V (𝑤𝑅𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧𝑅𝑤))
82		dfwe2 7774	. 2 ⊢ (𝑅 We V ↔ (𝑅 Fr V ∧ ∀𝑤 ∈ V ∀𝑧 ∈ V (𝑤𝑅𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧𝑅𝑤)))
83	51, 81, 82	sylanbrc 594	1 ⊢ (𝐹:V–1-1→On → 𝑅 We V)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ w3o 1102  ∀wal 1568   = wceq 1570   ∈ wcel 2143   ≠ wne 2958  ∀wral 3079  ∃wrex 3089  Vcvv 3455   ∩ cin 3905   ⊆ wss 3906  ∅c0 4287   class class class wbr 5110  {copab 5174   Fr wfr 5613   We wwe 5615  dom cdm 5663   “ cima 5666  Oncon0 6362   Fn wfn 6533  –1-1→wf1 6535  ‘cfv 6538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-tp 4595  df-op 4597  df-uni 4874  df-int 4914  df-br 5111  df-opab 5175  df-tr 5220  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-ord 6365  df-on 6366  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fv 6546

This theorem is referenced by:  vonf1owev  35571  onvfowev  35578