Theorem vonf1owevOLD 35862

Description: Obsolete version of vonf1owev 35861 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 6816	. . . . . . . 8 ⊢ (𝐹:V–1-1-onto→On → 𝐹:V⟶On)
2	1	fimassd 6723	. . . . . . 7 ⊢ (𝐹:V–1-1-onto→On → (𝐹 “ 𝑡) ⊆ On)
3		f1odm 6820	. . . . . . . . . . . 12 ⊢ (𝐹:V–1-1-onto→On → dom 𝐹 = V)
4	3	ineq1d 4165	. . . . . . . . . . 11 ⊢ (𝐹:V–1-1-onto→On → (dom 𝐹 ∩ 𝑡) = (V ∩ 𝑡))
5	4	neeq1d 3015	. . . . . . . . . 10 ⊢ (𝐹:V–1-1-onto→On → ((dom 𝐹 ∩ 𝑡) ≠ ∅ ↔ (V ∩ 𝑡) ≠ ∅))
6		inv1 4348	. . . . . . . . . . . 12 ⊢ (𝑡 ∩ V) = 𝑡
7	6	ineqcomi 4157	. . . . . . . . . . 11 ⊢ (V ∩ 𝑡) = 𝑡
8	7	neeq1i 3020	. . . . . . . . . 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 6075	. . . . . . 7 ⊢ ((𝐹:V–1-1-onto→On ∧ 𝑡 ≠ ∅) → (𝐹 “ 𝑡) ≠ ∅)
12		onssmin 7795	. . . . . . 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 3455	. . . . . . . . . . . 12 ⊢ 𝑣 ∈ V
16		vex 3455	. . . . . . . . . . . 12 ⊢ 𝑢 ∈ V
17		fveq2 6877	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑣 → (𝐹‘𝑥) = (𝐹‘𝑣))
18	17	eleq1d 2846	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑣 → ((𝐹‘𝑥) ∈ (𝐹‘𝑦) ↔ (𝐹‘𝑣) ∈ (𝐹‘𝑦)))
19		fveq2 6877	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑢 → (𝐹‘𝑦) = (𝐹‘𝑢))
20	19	eleq2d 2847	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑢 → ((𝐹‘𝑣) ∈ (𝐹‘𝑦) ↔ (𝐹‘𝑣) ∈ (𝐹‘𝑢)))
21		vonf1owevOLD.1	. . . . . . . . . . . 12 ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝐹‘𝑥) ∈ (𝐹‘𝑦)}
22	15, 16, 18, 20, 21	brab 5518	. . . . . . . . . . 11 ⊢ (𝑣𝑅𝑢 ↔ (𝐹‘𝑣) ∈ (𝐹‘𝑢))
23	22	notbii 323	. . . . . . . . . 10 ⊢ (¬ 𝑣𝑅𝑢 ↔ ¬ (𝐹‘𝑣) ∈ (𝐹‘𝑢))
24	1	ffvelcdmda 7076	. . . . . . . . . . . 12 ⊢ ((𝐹:V–1-1-onto→On ∧ 𝑢 ∈ V) → (𝐹‘𝑢) ∈ On)
25	24	elvd 3457	. . . . . . . . . . 11 ⊢ (𝐹:V–1-1-onto→On → (𝐹‘𝑢) ∈ On)
26	1	ffvelcdmda 7076	. . . . . . . . . . . 12 ⊢ ((𝐹:V–1-1-onto→On ∧ 𝑣 ∈ V) → (𝐹‘𝑣) ∈ On)
27	26	elvd 3457	. . . . . . . . . . 11 ⊢ (𝐹:V–1-1-onto→On → (𝐹‘𝑣) ∈ On)
28		ontri1 6390	. . . . . . . . . . 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 3186	. . . . . . . 8 ⊢ (𝐹:V–1-1-onto→On → (∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢 ↔ ∀𝑣 ∈ 𝑡 (𝐹‘𝑢) ⊆ (𝐹‘𝑣)))
32		f1ofn 6817	. . . . . . . . 9 ⊢ (𝐹:V–1-1-onto→On → 𝐹 Fn V)
33		ssv 3955	. . . . . . . . 9 ⊢ 𝑡 ⊆ V
34		sseq2 3957	. . . . . . . . . 10 ⊢ (𝑠 = (𝐹‘𝑣) → ((𝐹‘𝑢) ⊆ 𝑠 ↔ (𝐹‘𝑢) ⊆ (𝐹‘𝑣)))
35	34	ralima 7235	. . . . . . . . 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 3187	. . . . . 6 ⊢ (𝐹:V–1-1-onto→On → (∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢 ↔ ∃𝑢 ∈ 𝑡 ∀𝑠 ∈ (𝐹 “ 𝑡)(𝐹‘𝑢) ⊆ 𝑠))
39		sseq1 3956	. . . . . . . . 9 ⊢ (𝑟 = (𝐹‘𝑢) → (𝑟 ⊆ 𝑠 ↔ (𝐹‘𝑢) ⊆ 𝑠))
40	39	ralbidv 3186	. . . . . . . 8 ⊢ (𝑟 = (𝐹‘𝑢) → (∀𝑠 ∈ (𝐹 “ 𝑡)𝑟 ⊆ 𝑠 ↔ ∀𝑠 ∈ (𝐹 “ 𝑡)(𝐹‘𝑢) ⊆ 𝑠))
41	40	rexima 7236	. . . . . . 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 1960	. . 3 ⊢ (𝐹:V–1-1-onto→On → ∀𝑡(𝑡 ≠ ∅ → ∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢))
46		df-fr 5604	. . . 4 ⊢ (𝑅 Fr V ↔ ∀𝑡((𝑡 ⊆ V ∧ 𝑡 ≠ ∅) → ∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢))
47	33	biantrur 540	. . . . . 6 ⊢ (𝑡 ≠ ∅ ↔ (𝑡 ⊆ V ∧ 𝑡 ≠ ∅))
48	47	imbi1i 352	. . . . 5 ⊢ ((𝑡 ≠ ∅ → ∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢) ↔ ((𝑡 ⊆ V ∧ 𝑡 ≠ ∅) → ∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢))
49	48	albii 1852	. . . 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 7076	. . . . . . . 8 ⊢ ((𝐹:V–1-1-onto→On ∧ 𝑤 ∈ V) → (𝐹‘𝑤) ∈ On)
53	52	elvd 3457	. . . . . . 7 ⊢ (𝐹:V–1-1-onto→On → (𝐹‘𝑤) ∈ On)
54	1	ffvelcdmda 7076	. . . . . . . 8 ⊢ ((𝐹:V–1-1-onto→On ∧ 𝑧 ∈ V) → (𝐹‘𝑧) ∈ On)
55	54	elvd 3457	. . . . . . 7 ⊢ (𝐹:V–1-1-onto→On → (𝐹‘𝑧) ∈ On)
56		oneltri 6399	. . . . . . 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 3455	. . . . . . . . 9 ⊢ 𝑤 ∈ V
61		vex 3455	. . . . . . . . 9 ⊢ 𝑧 ∈ V
62		fveq2 6877	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → (𝐹‘𝑥) = (𝐹‘𝑤))
63	62	eleq1d 2846	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → ((𝐹‘𝑥) ∈ (𝐹‘𝑦) ↔ (𝐹‘𝑤) ∈ (𝐹‘𝑦)))
64		fveq2 6877	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧))
65	64	eleq2d 2847	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ((𝐹‘𝑤) ∈ (𝐹‘𝑦) ↔ (𝐹‘𝑤) ∈ (𝐹‘𝑧)))
66	60, 61, 63, 65, 21	brab 5518	. . . . . . . 8 ⊢ (𝑤𝑅𝑧 ↔ (𝐹‘𝑤) ∈ (𝐹‘𝑧))
67	66	biimpri 231	. . . . . . 7 ⊢ ((𝐹‘𝑤) ∈ (𝐹‘𝑧) → 𝑤𝑅𝑧)
68	67	a1i 11	. . . . . 6 ⊢ (𝐹:V–1-1-onto→On → ((𝐹‘𝑤) ∈ (𝐹‘𝑧) → 𝑤𝑅𝑧))
69		f1of1 6815	. . . . . . 7 ⊢ (𝐹:V–1-1-onto→On → 𝐹:V–1-1→On)
70		f1veqaeq 7252	. . . . . . . 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 6877	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
74	73	eleq1d 2846	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) ∈ (𝐹‘𝑦) ↔ (𝐹‘𝑧) ∈ (𝐹‘𝑦)))
75		fveq2 6877	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → (𝐹‘𝑦) = (𝐹‘𝑤))
76	75	eleq2d 2847	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → ((𝐹‘𝑧) ∈ (𝐹‘𝑦) ↔ (𝐹‘𝑧) ∈ (𝐹‘𝑤)))
77	61, 60, 74, 76, 21	brab 5518	. . . . . . . 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 3159	. . 3 ⊢ (𝐹:V–1-1-onto→On → ∀𝑧 ∈ V (𝑤𝑅𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧𝑅𝑤))
83	82	ralrimivw 3159	. 2 ⊢ (𝐹:V–1-1-onto→On → ∀𝑤 ∈ V ∀𝑧 ∈ V (𝑤𝑅𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧𝑅𝑤))
84		dfwe2 7777	. 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 1568   = wceq 1570   ∈ wcel 2145   ≠ wne 2956  ∀wral 3077  ∃wrex 3087  Vcvv 3451   ∩ cin 3898   ⊆ wss 3899  ∅c0 4279   class class class wbr 5103  {copab 5167   Fr wfr 5601   We wwe 5603  dom cdm 5651   “ cima 5654  Oncon0 6355   Fn wfn 6526  –1-1→wf1 6528  –1-1-onto→wf1o 6530  ‘cfv 6531

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-int 4908  df-br 5104  df-opab 5168  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-ord 6358  df-on 6359  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-f1o 6538  df-fv 6539

This theorem is used by: (None)