Theorem vonf1owev 35102

Description: If 𝐹 is a bijection from the universe to the ordinals, then 𝑅 well-orders the universe. This is the ZFC version of (2 → 3) in https://tinyurl.com/hamkins-gblac. (Contributed by BTernaryTau, 6-Dec-2025.)

Hypothesis

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

Assertion

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

Distinct variable group:   𝑥,𝐹,𝑦

Allowed substitution hints:   𝑅(𝑥,𝑦)

Proof of Theorem vonf1owev

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

Step	Hyp	Ref	Expression
1		f1of 6803	. . . . . . . 8 ⊢ (𝐹:V–1-1-onto→On → 𝐹:V⟶On)
2	1	fimassd 6712	. . . . . . 7 ⊢ (𝐹:V–1-1-onto→On → (𝐹 “ 𝑡) ⊆ On)
3		f1odm 6807	. . . . . . . . . . . 12 ⊢ (𝐹:V–1-1-onto→On → dom 𝐹 = V)
4	3	ineq1d 4185	. . . . . . . . . . 11 ⊢ (𝐹:V–1-1-onto→On → (dom 𝐹 ∩ 𝑡) = (V ∩ 𝑡))
5	4	neeq1d 2985	. . . . . . . . . 10 ⊢ (𝐹:V–1-1-onto→On → ((dom 𝐹 ∩ 𝑡) ≠ ∅ ↔ (V ∩ 𝑡) ≠ ∅))
6		inv1 4364	. . . . . . . . . . . 12 ⊢ (𝑡 ∩ V) = 𝑡
7	6	ineqcomi 4177	. . . . . . . . . . 11 ⊢ (V ∩ 𝑡) = 𝑡
8	7	neeq1i 2990	. . . . . . . . . 10 ⊢ ((V ∩ 𝑡) ≠ ∅ ↔ 𝑡 ≠ ∅)
9	5, 8	bitr2di 288	. . . . . . . . 9 ⊢ (𝐹:V–1-1-onto→On → (𝑡 ≠ ∅ ↔ (dom 𝐹 ∩ 𝑡) ≠ ∅))
10	9	biimpa 476	. . . . . . . 8 ⊢ ((𝐹:V–1-1-onto→On ∧ 𝑡 ≠ ∅) → (dom 𝐹 ∩ 𝑡) ≠ ∅)
11	10	imadisjlnd 6055	. . . . . . 7 ⊢ ((𝐹:V–1-1-onto→On ∧ 𝑡 ≠ ∅) → (𝐹 “ 𝑡) ≠ ∅)
12		onssmin 7771	. . . . . . 7 ⊢ (((𝐹 “ 𝑡) ⊆ On ∧ (𝐹 “ 𝑡) ≠ ∅) → ∃𝑟 ∈ (𝐹 “ 𝑡)∀𝑠 ∈ (𝐹 “ 𝑡)𝑟 ⊆ 𝑠)
13	2, 11, 12	syl2an2r 685	. . . . . 6 ⊢ ((𝐹:V–1-1-onto→On ∧ 𝑡 ≠ ∅) → ∃𝑟 ∈ (𝐹 “ 𝑡)∀𝑠 ∈ (𝐹 “ 𝑡)𝑟 ⊆ 𝑠)
14	13	ex 412	. . . . 5 ⊢ (𝐹:V–1-1-onto→On → (𝑡 ≠ ∅ → ∃𝑟 ∈ (𝐹 “ 𝑡)∀𝑠 ∈ (𝐹 “ 𝑡)𝑟 ⊆ 𝑠))
15		vex 3454	. . . . . . . . . . . 12 ⊢ 𝑣 ∈ V
16		vex 3454	. . . . . . . . . . . 12 ⊢ 𝑢 ∈ V
17		fveq2 6861	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑣 → (𝐹‘𝑥) = (𝐹‘𝑣))
18	17	eleq1d 2814	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑣 → ((𝐹‘𝑥) ∈ (𝐹‘𝑦) ↔ (𝐹‘𝑣) ∈ (𝐹‘𝑦)))
19		fveq2 6861	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑢 → (𝐹‘𝑦) = (𝐹‘𝑢))
20	19	eleq2d 2815	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑢 → ((𝐹‘𝑣) ∈ (𝐹‘𝑦) ↔ (𝐹‘𝑣) ∈ (𝐹‘𝑢)))
21		vonf1owev.1	. . . . . . . . . . . 12 ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝐹‘𝑥) ∈ (𝐹‘𝑦)}
22	15, 16, 18, 20, 21	brab 5506	. . . . . . . . . . 11 ⊢ (𝑣𝑅𝑢 ↔ (𝐹‘𝑣) ∈ (𝐹‘𝑢))
23	22	notbii 320	. . . . . . . . . 10 ⊢ (¬ 𝑣𝑅𝑢 ↔ ¬ (𝐹‘𝑣) ∈ (𝐹‘𝑢))
24	1	ffvelcdmda 7059	. . . . . . . . . . . 12 ⊢ ((𝐹:V–1-1-onto→On ∧ 𝑢 ∈ V) → (𝐹‘𝑢) ∈ On)
25	24	elvd 3456	. . . . . . . . . . 11 ⊢ (𝐹:V–1-1-onto→On → (𝐹‘𝑢) ∈ On)
26	1	ffvelcdmda 7059	. . . . . . . . . . . 12 ⊢ ((𝐹:V–1-1-onto→On ∧ 𝑣 ∈ V) → (𝐹‘𝑣) ∈ On)
27	26	elvd 3456	. . . . . . . . . . 11 ⊢ (𝐹:V–1-1-onto→On → (𝐹‘𝑣) ∈ On)
28		ontri1 6369	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑢) ∈ On ∧ (𝐹‘𝑣) ∈ On) → ((𝐹‘𝑢) ⊆ (𝐹‘𝑣) ↔ ¬ (𝐹‘𝑣) ∈ (𝐹‘𝑢)))
29	25, 27, 28	syl2anc 584	. . . . . . . . . 10 ⊢ (𝐹:V–1-1-onto→On → ((𝐹‘𝑢) ⊆ (𝐹‘𝑣) ↔ ¬ (𝐹‘𝑣) ∈ (𝐹‘𝑢)))
30	23, 29	bitr4id 290	. . . . . . . . 9 ⊢ (𝐹:V–1-1-onto→On → (¬ 𝑣𝑅𝑢 ↔ (𝐹‘𝑢) ⊆ (𝐹‘𝑣)))
31	30	ralbidv 3157	. . . . . . . 8 ⊢ (𝐹:V–1-1-onto→On → (∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢 ↔ ∀𝑣 ∈ 𝑡 (𝐹‘𝑢) ⊆ (𝐹‘𝑣)))
32		f1ofn 6804	. . . . . . . . 9 ⊢ (𝐹:V–1-1-onto→On → 𝐹 Fn V)
33		ssv 3974	. . . . . . . . 9 ⊢ 𝑡 ⊆ V
34		sseq2 3976	. . . . . . . . . 10 ⊢ (𝑠 = (𝐹‘𝑣) → ((𝐹‘𝑢) ⊆ 𝑠 ↔ (𝐹‘𝑢) ⊆ (𝐹‘𝑣)))
35	34	ralima 7214	. . . . . . . . 9 ⊢ ((𝐹 Fn V ∧ 𝑡 ⊆ V) → (∀𝑠 ∈ (𝐹 “ 𝑡)(𝐹‘𝑢) ⊆ 𝑠 ↔ ∀𝑣 ∈ 𝑡 (𝐹‘𝑢) ⊆ (𝐹‘𝑣)))
36	32, 33, 35	sylancl 586	. . . . . . . 8 ⊢ (𝐹:V–1-1-onto→On → (∀𝑠 ∈ (𝐹 “ 𝑡)(𝐹‘𝑢) ⊆ 𝑠 ↔ ∀𝑣 ∈ 𝑡 (𝐹‘𝑢) ⊆ (𝐹‘𝑣)))
37	31, 36	bitr4d 282	. . . . . . 7 ⊢ (𝐹:V–1-1-onto→On → (∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢 ↔ ∀𝑠 ∈ (𝐹 “ 𝑡)(𝐹‘𝑢) ⊆ 𝑠))
38	37	rexbidv 3158	. . . . . 6 ⊢ (𝐹:V–1-1-onto→On → (∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢 ↔ ∃𝑢 ∈ 𝑡 ∀𝑠 ∈ (𝐹 “ 𝑡)(𝐹‘𝑢) ⊆ 𝑠))
39		sseq1 3975	. . . . . . . . 9 ⊢ (𝑟 = (𝐹‘𝑢) → (𝑟 ⊆ 𝑠 ↔ (𝐹‘𝑢) ⊆ 𝑠))
40	39	ralbidv 3157	. . . . . . . 8 ⊢ (𝑟 = (𝐹‘𝑢) → (∀𝑠 ∈ (𝐹 “ 𝑡)𝑟 ⊆ 𝑠 ↔ ∀𝑠 ∈ (𝐹 “ 𝑡)(𝐹‘𝑢) ⊆ 𝑠))
41	40	rexima 7215	. . . . . . 7 ⊢ ((𝐹 Fn V ∧ 𝑡 ⊆ V) → (∃𝑟 ∈ (𝐹 “ 𝑡)∀𝑠 ∈ (𝐹 “ 𝑡)𝑟 ⊆ 𝑠 ↔ ∃𝑢 ∈ 𝑡 ∀𝑠 ∈ (𝐹 “ 𝑡)(𝐹‘𝑢) ⊆ 𝑠))
42	32, 33, 41	sylancl 586	. . . . . 6 ⊢ (𝐹:V–1-1-onto→On → (∃𝑟 ∈ (𝐹 “ 𝑡)∀𝑠 ∈ (𝐹 “ 𝑡)𝑟 ⊆ 𝑠 ↔ ∃𝑢 ∈ 𝑡 ∀𝑠 ∈ (𝐹 “ 𝑡)(𝐹‘𝑢) ⊆ 𝑠))
43	38, 42	bitr4d 282	. . . . 5 ⊢ (𝐹:V–1-1-onto→On → (∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢 ↔ ∃𝑟 ∈ (𝐹 “ 𝑡)∀𝑠 ∈ (𝐹 “ 𝑡)𝑟 ⊆ 𝑠))
44	14, 43	sylibrd 259	. . . 4 ⊢ (𝐹:V–1-1-onto→On → (𝑡 ≠ ∅ → ∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢))
45	44	alrimiv 1927	. . 3 ⊢ (𝐹:V–1-1-onto→On → ∀𝑡(𝑡 ≠ ∅ → ∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢))
46		df-fr 5594	. . . 4 ⊢ (𝑅 Fr V ↔ ∀𝑡((𝑡 ⊆ V ∧ 𝑡 ≠ ∅) → ∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢))
47	33	biantrur 530	. . . . . 6 ⊢ (𝑡 ≠ ∅ ↔ (𝑡 ⊆ V ∧ 𝑡 ≠ ∅))
48	47	imbi1i 349	. . . . 5 ⊢ ((𝑡 ≠ ∅ → ∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢) ↔ ((𝑡 ⊆ V ∧ 𝑡 ≠ ∅) → ∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢))
49	48	albii 1819	. . . 4 ⊢ (∀𝑡(𝑡 ≠ ∅ → ∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢) ↔ ∀𝑡((𝑡 ⊆ V ∧ 𝑡 ≠ ∅) → ∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢))
50	46, 49	bitr4i 278	. . 3 ⊢ (𝑅 Fr V ↔ ∀𝑡(𝑡 ≠ ∅ → ∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢))
51	45, 50	sylibr 234	. 2 ⊢ (𝐹:V–1-1-onto→On → 𝑅 Fr V)
52	1	ffvelcdmda 7059	. . . . . . . 8 ⊢ ((𝐹:V–1-1-onto→On ∧ 𝑤 ∈ V) → (𝐹‘𝑤) ∈ On)
53	52	elvd 3456	. . . . . . 7 ⊢ (𝐹:V–1-1-onto→On → (𝐹‘𝑤) ∈ On)
54	1	ffvelcdmda 7059	. . . . . . . 8 ⊢ ((𝐹:V–1-1-onto→On ∧ 𝑧 ∈ V) → (𝐹‘𝑧) ∈ On)
55	54	elvd 3456	. . . . . . 7 ⊢ (𝐹:V–1-1-onto→On → (𝐹‘𝑧) ∈ On)
56		oneltri 6378	. . . . . . 7 ⊢ (((𝐹‘𝑤) ∈ On ∧ (𝐹‘𝑧) ∈ On) → ((𝐹‘𝑤) ∈ (𝐹‘𝑧) ∨ (𝐹‘𝑧) ∈ (𝐹‘𝑤) ∨ (𝐹‘𝑤) = (𝐹‘𝑧)))
57	53, 55, 56	syl2anc 584	. . . . . 6 ⊢ (𝐹:V–1-1-onto→On → ((𝐹‘𝑤) ∈ (𝐹‘𝑧) ∨ (𝐹‘𝑧) ∈ (𝐹‘𝑤) ∨ (𝐹‘𝑤) = (𝐹‘𝑧)))
58		3orcomb 1093	. . . . . 6 ⊢ (((𝐹‘𝑤) ∈ (𝐹‘𝑧) ∨ (𝐹‘𝑧) ∈ (𝐹‘𝑤) ∨ (𝐹‘𝑤) = (𝐹‘𝑧)) ↔ ((𝐹‘𝑤) ∈ (𝐹‘𝑧) ∨ (𝐹‘𝑤) = (𝐹‘𝑧) ∨ (𝐹‘𝑧) ∈ (𝐹‘𝑤)))
59	57, 58	sylib 218	. . . . 5 ⊢ (𝐹:V–1-1-onto→On → ((𝐹‘𝑤) ∈ (𝐹‘𝑧) ∨ (𝐹‘𝑤) = (𝐹‘𝑧) ∨ (𝐹‘𝑧) ∈ (𝐹‘𝑤)))
60		vex 3454	. . . . . . . . 9 ⊢ 𝑤 ∈ V
61		vex 3454	. . . . . . . . 9 ⊢ 𝑧 ∈ V
62		fveq2 6861	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → (𝐹‘𝑥) = (𝐹‘𝑤))
63	62	eleq1d 2814	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → ((𝐹‘𝑥) ∈ (𝐹‘𝑦) ↔ (𝐹‘𝑤) ∈ (𝐹‘𝑦)))
64		fveq2 6861	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧))
65	64	eleq2d 2815	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ((𝐹‘𝑤) ∈ (𝐹‘𝑦) ↔ (𝐹‘𝑤) ∈ (𝐹‘𝑧)))
66	60, 61, 63, 65, 21	brab 5506	. . . . . . . 8 ⊢ (𝑤𝑅𝑧 ↔ (𝐹‘𝑤) ∈ (𝐹‘𝑧))
67	66	biimpri 228	. . . . . . 7 ⊢ ((𝐹‘𝑤) ∈ (𝐹‘𝑧) → 𝑤𝑅𝑧)
68	67	a1i 11	. . . . . 6 ⊢ (𝐹:V–1-1-onto→On → ((𝐹‘𝑤) ∈ (𝐹‘𝑧) → 𝑤𝑅𝑧))
69		f1of1 6802	. . . . . . 7 ⊢ (𝐹:V–1-1-onto→On → 𝐹:V–1-1→On)
70		f1veqaeq 7234	. . . . . . . 8 ⊢ ((𝐹:V–1-1→On ∧ (𝑤 ∈ V ∧ 𝑧 ∈ V)) → ((𝐹‘𝑤) = (𝐹‘𝑧) → 𝑤 = 𝑧))
71	60, 61, 70	mpanr12 705	. . . . . . 7 ⊢ (𝐹:V–1-1→On → ((𝐹‘𝑤) = (𝐹‘𝑧) → 𝑤 = 𝑧))
72	69, 71	syl 17	. . . . . 6 ⊢ (𝐹:V–1-1-onto→On → ((𝐹‘𝑤) = (𝐹‘𝑧) → 𝑤 = 𝑧))
73		fveq2 6861	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
74	73	eleq1d 2814	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) ∈ (𝐹‘𝑦) ↔ (𝐹‘𝑧) ∈ (𝐹‘𝑦)))
75		fveq2 6861	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → (𝐹‘𝑦) = (𝐹‘𝑤))
76	75	eleq2d 2815	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → ((𝐹‘𝑧) ∈ (𝐹‘𝑦) ↔ (𝐹‘𝑧) ∈ (𝐹‘𝑤)))
77	61, 60, 74, 76, 21	brab 5506	. . . . . . . 8 ⊢ (𝑧𝑅𝑤 ↔ (𝐹‘𝑧) ∈ (𝐹‘𝑤))
78	77	biimpri 228	. . . . . . 7 ⊢ ((𝐹‘𝑧) ∈ (𝐹‘𝑤) → 𝑧𝑅𝑤)
79	78	a1i 11	. . . . . 6 ⊢ (𝐹:V–1-1-onto→On → ((𝐹‘𝑧) ∈ (𝐹‘𝑤) → 𝑧𝑅𝑤))
80	68, 72, 79	3orim123d 1446	. . . . 5 ⊢ (𝐹:V–1-1-onto→On → (((𝐹‘𝑤) ∈ (𝐹‘𝑧) ∨ (𝐹‘𝑤) = (𝐹‘𝑧) ∨ (𝐹‘𝑧) ∈ (𝐹‘𝑤)) → (𝑤𝑅𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧𝑅𝑤)))
81	59, 80	mpd 15	. . . 4 ⊢ (𝐹:V–1-1-onto→On → (𝑤𝑅𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧𝑅𝑤))
82	81	ralrimivw 3130	. . 3 ⊢ (𝐹:V–1-1-onto→On → ∀𝑧 ∈ V (𝑤𝑅𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧𝑅𝑤))
83	82	ralrimivw 3130	. 2 ⊢ (𝐹:V–1-1-onto→On → ∀𝑤 ∈ V ∀𝑧 ∈ V (𝑤𝑅𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧𝑅𝑤))
84		dfwe2 7753	. 2 ⊢ (𝑅 We V ↔ (𝑅 Fr V ∧ ∀𝑤 ∈ V ∀𝑧 ∈ V (𝑤𝑅𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧𝑅𝑤)))
85	51, 83, 84	sylanbrc 583	1 ⊢ (𝐹:V–1-1-onto→On → 𝑅 We V)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ w3o 1085  ∀wal 1538   = wceq 1540   ∈ wcel 2109   ≠ wne 2926  ∀wral 3045  ∃wrex 3054  Vcvv 3450   ∩ cin 3916   ⊆ wss 3917  ∅c0 4299   class class class wbr 5110  {copab 5172   Fr wfr 5591   We wwe 5593  dom cdm 5641   “ cima 5644  Oncon0 6335   Fn wfn 6509  –1-1→wf1 6511  –1-1-onto→wf1o 6513  ‘cfv 6514

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-tp 4597  df-op 4599  df-uni 4875  df-int 4914  df-br 5111  df-opab 5173  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-ord 6338  df-on 6339  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-f1o 6521  df-fv 6522

This theorem is referenced by: (None)