Theorem vonf1owevOLD 35957

Description: Obsolete version of vonf1owev 35956 as of 11-Jun-2026. (Contributed by BTernaryTau, 6-Dec-2025.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis

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

Assertion

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

Distinct variable group:   𝑥,𝐹,𝑦

Allowed substitution hints:   𝑅(𝑥, 𝑦)

Proof of Theorem vonf1owevOLD

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

Step	Hyp	Ref	Expression
1		f1of 6824	. . . . . . . 8 ⊢ (𝐹:V–1-1-onto→On → 𝐹:V⟶On)
2	1	fimassd 6731	. . . . . . 7 ⊢ (𝐹:V–1-1-onto→On → (𝐹 “ 𝑡) ⊆ On)
3		f1odm 6828	. . . . . . . . . . . 12 ⊢ (𝐹:V–1-1-onto→On → dom 𝐹 = V)
4	3	ineq1d 4116	. . . . . . . . . . 11 ⊢ (𝐹:V–1-1-onto→On → (dom 𝐹 ∩ 𝑡) = (V ∩ 𝑡))
5	4	neeq1d 3014	. . . . . . . . . 10 ⊢ (𝐹:V–1-1-onto→On → ((dom 𝐹 ∩ 𝑡) ≠ ∅ ↔ (V ∩ 𝑡) ≠ ∅))
6		inv1 4347	. . . . . . . . . . . 12 ⊢ (𝑡 ∩ V) = 𝑡
7	6	ineqcomi 4108	. . . . . . . . . . 11 ⊢ (V ∩ 𝑡) = 𝑡
8	7	neeq1i 3019	. . . . . . . . . 10 ⊢ ((V ∩ 𝑡) ≠ ∅ ↔ 𝑡 ≠ ∅)
9	5, 8	bitr2di 291	. . . . . . . . 9 ⊢ (𝐹:V–1-1-onto→On → (𝑡 ≠ ∅ ↔ (dom 𝐹 ∩ 𝑡) ≠ ∅))
10	9	biimpa 482	. . . . . . . 8 ⊢ ((𝐹:V–1-1-onto→On ∧ 𝑡 ≠ ∅) → (dom 𝐹 ∩ 𝑡) ≠ ∅)
11	10	imadisjlnd 6077	. . . . . . 7 ⊢ ((𝐹:V–1-1-onto→On ∧ 𝑡 ≠ ∅) → (𝐹 “ 𝑡) ≠ ∅)
12		onssmin 7806	. . . . . . 7 ⊢ (((𝐹 “ 𝑡) ⊆ On ∧ (𝐹 “ 𝑡) ≠ ∅) → ∃𝑟 ∈ (𝐹 “ 𝑡)∀𝑠 ∈ (𝐹 “ 𝑡)𝑟 ⊆ 𝑠)
13	2, 11, 12	syl2an2r 698	. . . . . 6 ⊢ ((𝐹:V–1-1-onto→On ∧ 𝑡 ≠ ∅) → ∃𝑟 ∈ (𝐹 “ 𝑡)∀𝑠 ∈ (𝐹 “ 𝑡)𝑟 ⊆ 𝑠)
14	13	ex 418	. . . . 5 ⊢ (𝐹:V–1-1-onto→On → (𝑡 ≠ ∅ → ∃𝑟 ∈ (𝐹 “ 𝑡)∀𝑠 ∈ (𝐹 “ 𝑡)𝑟 ⊆ 𝑠))
15		vex 3454	. . . . . . . . . . . 12 ⊢ 𝑣 ∈ V
16		vex 3454	. . . . . . . . . . . 12 ⊢ 𝑢 ∈ V
17		fveq2 6885	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑣 → (𝐹‘𝑥) = (𝐹‘𝑣))
18	17	eleq1d 2845	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑣 → ((𝐹‘𝑥) ∈ (𝐹‘𝑦) ↔ (𝐹‘𝑣) ∈ (𝐹‘𝑦)))
19		fveq2 6885	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑢 → (𝐹‘𝑦) = (𝐹‘𝑢))
20	19	eleq2d 2846	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑢 → ((𝐹‘𝑣) ∈ (𝐹‘𝑦) ↔ (𝐹‘𝑣) ∈ (𝐹‘𝑢)))
21		vonf1owevOLD.1	. . . . . . . . . . . 12 ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝐹‘𝑥) ∈ (𝐹‘𝑦)}
22	15, 16, 18, 20, 21	brab 5517	. . . . . . . . . . 11 ⊢ (𝑣𝑅𝑢 ↔ (𝐹‘𝑣) ∈ (𝐹‘𝑢))
23	22	notbii 323	. . . . . . . . . 10 ⊢ (¬ 𝑣𝑅𝑢 ↔ ¬ (𝐹‘𝑣) ∈ (𝐹‘𝑢))
24	1	ffvelcdmda 7084	. . . . . . . . . . . 12 ⊢ ((𝐹:V–1-1-onto→On ∧ 𝑢 ∈ V) → (𝐹‘𝑢) ∈ On)
25	24	elvd 3456	. . . . . . . . . . 11 ⊢ (𝐹:V–1-1-onto→On → (𝐹‘𝑢) ∈ On)
26	1	ffvelcdmda 7084	. . . . . . . . . . . 12 ⊢ ((𝐹:V–1-1-onto→On ∧ 𝑣 ∈ V) → (𝐹‘𝑣) ∈ On)
27	26	elvd 3456	. . . . . . . . . . 11 ⊢ (𝐹:V–1-1-onto→On → (𝐹‘𝑣) ∈ On)
28		ontri1 6397	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑢) ∈ On ∧ (𝐹‘𝑣) ∈ On) → ((𝐹‘𝑢) ⊆ (𝐹‘𝑣) ↔ ¬ (𝐹‘𝑣) ∈ (𝐹‘𝑢)))
29	25, 27, 28	syl2anc 596	. . . . . . . . . 10 ⊢ (𝐹:V–1-1-onto→On → ((𝐹‘𝑢) ⊆ (𝐹‘𝑣) ↔ ¬ (𝐹‘𝑣) ∈ (𝐹‘𝑢)))
30	23, 29	bitr4id 293	. . . . . . . . 9 ⊢ (𝐹:V–1-1-onto→On → (¬ 𝑣𝑅𝑢 ↔ (𝐹‘𝑢) ⊆ (𝐹‘𝑣)))
31	30	ralbidv 3185	. . . . . . . 8 ⊢ (𝐹:V–1-1-onto→On → (∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢 ↔ ∀𝑣 ∈ 𝑡 (𝐹‘𝑢) ⊆ (𝐹‘𝑣)))
32		f1ofn 6825	. . . . . . . . 9 ⊢ (𝐹:V–1-1-onto→On → 𝐹 Fn V)
33		ssv 3932	. . . . . . . . 9 ⊢ 𝑡 ⊆ V
34		sseq2 3934	. . . . . . . . . 10 ⊢ (𝑠 = (𝐹‘𝑣) → ((𝐹‘𝑢) ⊆ 𝑠 ↔ (𝐹‘𝑢) ⊆ (𝐹‘𝑣)))
35	34	ralima 7243	. . . . . . . . 9 ⊢ ((𝐹 Fn V ∧ 𝑡 ⊆ V) → (∀𝑠 ∈ (𝐹 “ 𝑡)(𝐹‘𝑢) ⊆ 𝑠 ↔ ∀𝑣 ∈ 𝑡 (𝐹‘𝑢) ⊆ (𝐹‘𝑣)))
36	32, 33, 35	sylancl 598	. . . . . . . 8 ⊢ (𝐹:V–1-1-onto→On → (∀𝑠 ∈ (𝐹 “ 𝑡)(𝐹‘𝑢) ⊆ 𝑠 ↔ ∀𝑣 ∈ 𝑡 (𝐹‘𝑢) ⊆ (𝐹‘𝑣)))
37	31, 36	bitr4d 285	. . . . . . 7 ⊢ (𝐹:V–1-1-onto→On → (∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢 ↔ ∀𝑠 ∈ (𝐹 “ 𝑡)(𝐹‘𝑢) ⊆ 𝑠))
38	37	rexbidv 3186	. . . . . 6 ⊢ (𝐹:V–1-1-onto→On → (∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢 ↔ ∃𝑢 ∈ 𝑡 ∀𝑠 ∈ (𝐹 “ 𝑡)(𝐹‘𝑢) ⊆ 𝑠))
39		sseq1 3933	. . . . . . . . 9 ⊢ (𝑟 = (𝐹‘𝑢) → (𝑟 ⊆ 𝑠 ↔ (𝐹‘𝑢) ⊆ 𝑠))
40	39	ralbidv 3185	. . . . . . . 8 ⊢ (𝑟 = (𝐹‘𝑢) → (∀𝑠 ∈ (𝐹 “ 𝑡)𝑟 ⊆ 𝑠 ↔ ∀𝑠 ∈ (𝐹 “ 𝑡)(𝐹‘𝑢) ⊆ 𝑠))
41	40	rexima 7244	. . . . . . 7 ⊢ ((𝐹 Fn V ∧ 𝑡 ⊆ V) → (∃𝑟 ∈ (𝐹 “ 𝑡)∀𝑠 ∈ (𝐹 “ 𝑡)𝑟 ⊆ 𝑠 ↔ ∃𝑢 ∈ 𝑡 ∀𝑠 ∈ (𝐹 “ 𝑡)(𝐹‘𝑢) ⊆ 𝑠))
42	32, 33, 41	sylancl 598	. . . . . 6 ⊢ (𝐹:V–1-1-onto→On → (∃𝑟 ∈ (𝐹 “ 𝑡)∀𝑠 ∈ (𝐹 “ 𝑡)𝑟 ⊆ 𝑠 ↔ ∃𝑢 ∈ 𝑡 ∀𝑠 ∈ (𝐹 “ 𝑡)(𝐹‘𝑢) ⊆ 𝑠))
43	38, 42	bitr4d 285	. . . . 5 ⊢ (𝐹:V–1-1-onto→On → (∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢 ↔ ∃𝑟 ∈ (𝐹 “ 𝑡)∀𝑠 ∈ (𝐹 “ 𝑡)𝑟 ⊆ 𝑠))
44	14, 43	sylibrd 262	. . . 4 ⊢ (𝐹:V–1-1-onto→On → (𝑡 ≠ ∅ → ∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢))
45	44	alrimiv 1959	. . 3 ⊢ (𝐹:V–1-1-onto→On → ∀𝑡(𝑡 ≠ ∅ → ∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢))
46		df-fr 5603	. . . 4 ⊢ (𝑅 Fr V ↔ ∀𝑡((𝑡 ⊆ V ∧ 𝑡 ≠ ∅) → ∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢))
47	33	biantrur 540	. . . . . 6 ⊢ (𝑡 ≠ ∅ ↔ (𝑡 ⊆ V ∧ 𝑡 ≠ ∅))
48	47	imbi1i 352	. . . . 5 ⊢ ((𝑡 ≠ ∅ → ∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢) ↔ ((𝑡 ⊆ V ∧ 𝑡 ≠ ∅) → ∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢))
49	48	albii 1851	. . . 4 ⊢ (∀𝑡(𝑡 ≠ ∅ → ∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢) ↔ ∀𝑡((𝑡 ⊆ V ∧ 𝑡 ≠ ∅) → ∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢))
50	46, 49	bitr4i 281	. . 3 ⊢ (𝑅 Fr V ↔ ∀𝑡(𝑡 ≠ ∅ → ∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢))
51	45, 50	sylibr 237	. 2 ⊢ (𝐹:V–1-1-onto→On → 𝑅 Fr V)
52	1	ffvelcdmda 7084	. . . . . . . 8 ⊢ ((𝐹:V–1-1-onto→On ∧ 𝑤 ∈ V) → (𝐹‘𝑤) ∈ On)
53	52	elvd 3456	. . . . . . 7 ⊢ (𝐹:V–1-1-onto→On → (𝐹‘𝑤) ∈ On)
54	1	ffvelcdmda 7084	. . . . . . . 8 ⊢ ((𝐹:V–1-1-onto→On ∧ 𝑧 ∈ V) → (𝐹‘𝑧) ∈ On)
55	54	elvd 3456	. . . . . . 7 ⊢ (𝐹:V–1-1-onto→On → (𝐹‘𝑧) ∈ On)
56		oneltri 6406	. . . . . . 7 ⊢ (((𝐹‘𝑤) ∈ On ∧ (𝐹‘𝑧) ∈ On) → ((𝐹‘𝑤) ∈ (𝐹‘𝑧) ∨ (𝐹‘𝑧) ∈ (𝐹‘𝑤) ∨ (𝐹‘𝑤) = (𝐹‘𝑧)))
57	53, 55, 56	syl2anc 596	. . . . . 6 ⊢ (𝐹:V–1-1-onto→On → ((𝐹‘𝑤) ∈ (𝐹‘𝑧) ∨ (𝐹‘𝑧) ∈ (𝐹‘𝑤) ∨ (𝐹‘𝑤) = (𝐹‘𝑧)))
58		3orcomb 1110	. . . . . 6 ⊢ (((𝐹‘𝑤) ∈ (𝐹‘𝑧) ∨ (𝐹‘𝑧) ∈ (𝐹‘𝑤) ∨ (𝐹‘𝑤) = (𝐹‘𝑧)) ↔ ((𝐹‘𝑤) ∈ (𝐹‘𝑧) ∨ (𝐹‘𝑤) = (𝐹‘𝑧) ∨ (𝐹‘𝑧) ∈ (𝐹‘𝑤)))
59	57, 58	sylib 221	. . . . 5 ⊢ (𝐹:V–1-1-onto→On → ((𝐹‘𝑤) ∈ (𝐹‘𝑧) ∨ (𝐹‘𝑤) = (𝐹‘𝑧) ∨ (𝐹‘𝑧) ∈ (𝐹‘𝑤)))
60		vex 3454	. . . . . . . . 9 ⊢ 𝑤 ∈ V
61		vex 3454	. . . . . . . . 9 ⊢ 𝑧 ∈ V
62		fveq2 6885	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → (𝐹‘𝑥) = (𝐹‘𝑤))
63	62	eleq1d 2845	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → ((𝐹‘𝑥) ∈ (𝐹‘𝑦) ↔ (𝐹‘𝑤) ∈ (𝐹‘𝑦)))
64		fveq2 6885	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧))
65	64	eleq2d 2846	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ((𝐹‘𝑤) ∈ (𝐹‘𝑦) ↔ (𝐹‘𝑤) ∈ (𝐹‘𝑧)))
66	60, 61, 63, 65, 21	brab 5517	. . . . . . . 8 ⊢ (𝑤𝑅𝑧 ↔ (𝐹‘𝑤) ∈ (𝐹‘𝑧))
67	66	biimpri 231	. . . . . . 7 ⊢ ((𝐹‘𝑤) ∈ (𝐹‘𝑧) → 𝑤𝑅𝑧)
68	67	a1i 11	. . . . . 6 ⊢ (𝐹:V–1-1-onto→On → ((𝐹‘𝑤) ∈ (𝐹‘𝑧) → 𝑤𝑅𝑧))
69		f1of1 6823	. . . . . . 7 ⊢ (𝐹:V–1-1-onto→On → 𝐹:V–1-1→On)
70		f1veqaeq 7260	. . . . . . . 8 ⊢ ((𝐹:V–1-1→On ∧ (𝑤 ∈ V ∧ 𝑧 ∈ V)) → ((𝐹‘𝑤) = (𝐹‘𝑧) → 𝑤 = 𝑧))
71	60, 61, 70	mpanr12 718	. . . . . . 7 ⊢ (𝐹:V–1-1→On → ((𝐹‘𝑤) = (𝐹‘𝑧) → 𝑤 = 𝑧))
72	69, 71	syl 18	. . . . . 6 ⊢ (𝐹:V–1-1-onto→On → ((𝐹‘𝑤) = (𝐹‘𝑧) → 𝑤 = 𝑧))
73		fveq2 6885	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
74	73	eleq1d 2845	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) ∈ (𝐹‘𝑦) ↔ (𝐹‘𝑧) ∈ (𝐹‘𝑦)))
75		fveq2 6885	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → (𝐹‘𝑦) = (𝐹‘𝑤))
76	75	eleq2d 2846	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → ((𝐹‘𝑧) ∈ (𝐹‘𝑦) ↔ (𝐹‘𝑧) ∈ (𝐹‘𝑤)))
77	61, 60, 74, 76, 21	brab 5517	. . . . . . . 8 ⊢ (𝑧𝑅𝑤 ↔ (𝐹‘𝑧) ∈ (𝐹‘𝑤))
78	77	biimpri 231	. . . . . . 7 ⊢ ((𝐹‘𝑧) ∈ (𝐹‘𝑤) → 𝑧𝑅𝑤)
79	78	a1i 11	. . . . . 6 ⊢ (𝐹:V–1-1-onto→On → ((𝐹‘𝑧) ∈ (𝐹‘𝑤) → 𝑧𝑅𝑤))
80	68, 72, 79	3orim123d 1472	. . . . 5 ⊢ (𝐹:V–1-1-onto→On → (((𝐹‘𝑤) ∈ (𝐹‘𝑧) ∨ (𝐹‘𝑤) = (𝐹‘𝑧) ∨ (𝐹‘𝑧) ∈ (𝐹‘𝑤)) → (𝑤𝑅𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧𝑅𝑤)))
81	59, 80	mpd 16	. . . 4 ⊢ (𝐹:V–1-1-onto→On → (𝑤𝑅𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧𝑅𝑤))
82	81	ralrimivw 3158	. . 3 ⊢ (𝐹:V–1-1-onto→On → ∀𝑧 ∈ V (𝑤𝑅𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧𝑅𝑤))
83	82	ralrimivw 3158	. 2 ⊢ (𝐹:V–1-1-onto→On → ∀𝑤 ∈ V ∀𝑧 ∈ V (𝑤𝑅𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧𝑅𝑤))
84		dfwe2 7788	. 2 ⊢ (𝑅 We V ↔ (𝑅 Fr V ∧ ∀𝑤 ∈ V ∀𝑧 ∈ V (𝑤𝑅𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧𝑅𝑤)))
85	51, 83, 84	sylanbrc 595	1 ⊢ (𝐹:V–1-1-onto→On → 𝑅 We V)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ w3o 1102  ∀wal 1567   = wceq 1569   ∈ wcel 2144   ≠ wne 2955  ∀wral 3076  ∃wrex 3086  Vcvv 3450   ⊆ wss 3895   ∩ cin 4089  ∅c0 4278   class class class wbr 5102  {copab 5166   Fr wfr 5600   We wwe 5602  dom cdm 5650   “ cima 5653  Oncon0 6362   Fn wfn 6533  –1-1→wf1 6535  –1-1-onto→wf1o 6537  ‘cfv 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4835  df-uni 4867  df-int 4907  df-br 5103  df-opab 5167  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-ord 6365  df-on 6366  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-f1o 6545  df-fv 6546

This theorem is used by: (None)