Theorem vonf1owevOLD 35618

Description: Obsolete version of vonf1owev 35617 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 6827	. . . . . . . 8 ⊢ (𝐹:V–1-1-onto→On → 𝐹:V⟶On)
2	1	fimassd 6734	. . . . . . 7 ⊢ (𝐹:V–1-1-onto→On → (𝐹 “ 𝑡) ⊆ On)
3		f1odm 6831	. . . . . . . . . . . 12 ⊢ (𝐹:V–1-1-onto→On → dom 𝐹 = V)
4	3	ineq1d 4175	. . . . . . . . . . 11 ⊢ (𝐹:V–1-1-onto→On → (dom 𝐹 ∩ 𝑡) = (V ∩ 𝑡))
5	4	neeq1d 3020	. . . . . . . . . 10 ⊢ (𝐹:V–1-1-onto→On → ((dom 𝐹 ∩ 𝑡) ≠ ∅ ↔ (V ∩ 𝑡) ≠ ∅))
6		inv1 4358	. . . . . . . . . . . 12 ⊢ (𝑡 ∩ V) = 𝑡
7	6	ineqcomi 4167	. . . . . . . . . . 11 ⊢ (V ∩ 𝑡) = 𝑡
8	7	neeq1i 3025	. . . . . . . . . 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 6088	. . . . . . 7 ⊢ ((𝐹:V–1-1-onto→On ∧ 𝑡 ≠ ∅) → (𝐹 “ 𝑡) ≠ ∅)
12		onssmin 7800	. . . . . . 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 3462	. . . . . . . . . . . 12 ⊢ 𝑣 ∈ V
16		vex 3462	. . . . . . . . . . . 12 ⊢ 𝑢 ∈ V
17		fveq2 6888	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑣 → (𝐹‘𝑥) = (𝐹‘𝑣))
18	17	eleq1d 2851	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑣 → ((𝐹‘𝑥) ∈ (𝐹‘𝑦) ↔ (𝐹‘𝑣) ∈ (𝐹‘𝑦)))
19		fveq2 6888	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑢 → (𝐹‘𝑦) = (𝐹‘𝑢))
20	19	eleq2d 2852	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑢 → ((𝐹‘𝑣) ∈ (𝐹‘𝑦) ↔ (𝐹‘𝑣) ∈ (𝐹‘𝑢)))
21		vonf1owevOLD.1	. . . . . . . . . . . 12 ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝐹‘𝑥) ∈ (𝐹‘𝑦)}
22	15, 16, 18, 20, 21	brab 5533	. . . . . . . . . . 11 ⊢ (𝑣𝑅𝑢 ↔ (𝐹‘𝑣) ∈ (𝐹‘𝑢))
23	22	notbii 323	. . . . . . . . . 10 ⊢ (¬ 𝑣𝑅𝑢 ↔ ¬ (𝐹‘𝑣) ∈ (𝐹‘𝑢))
24	1	ffvelcdmda 7086	. . . . . . . . . . . 12 ⊢ ((𝐹:V–1-1-onto→On ∧ 𝑢 ∈ V) → (𝐹‘𝑢) ∈ On)
25	24	elvd 3464	. . . . . . . . . . 11 ⊢ (𝐹:V–1-1-onto→On → (𝐹‘𝑢) ∈ On)
26	1	ffvelcdmda 7086	. . . . . . . . . . . 12 ⊢ ((𝐹:V–1-1-onto→On ∧ 𝑣 ∈ V) → (𝐹‘𝑣) ∈ On)
27	26	elvd 3464	. . . . . . . . . . 11 ⊢ (𝐹:V–1-1-onto→On → (𝐹‘𝑣) ∈ On)
28		ontri1 6402	. . . . . . . . . . 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 3191	. . . . . . . 8 ⊢ (𝐹:V–1-1-onto→On → (∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢 ↔ ∀𝑣 ∈ 𝑡 (𝐹‘𝑢) ⊆ (𝐹‘𝑣)))
32		f1ofn 6828	. . . . . . . . 9 ⊢ (𝐹:V–1-1-onto→On → 𝐹 Fn V)
33		ssv 3964	. . . . . . . . 9 ⊢ 𝑡 ⊆ V
34		sseq2 3966	. . . . . . . . . 10 ⊢ (𝑠 = (𝐹‘𝑣) → ((𝐹‘𝑢) ⊆ 𝑠 ↔ (𝐹‘𝑢) ⊆ (𝐹‘𝑣)))
35	34	ralima 7242	. . . . . . . . 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 3192	. . . . . 6 ⊢ (𝐹:V–1-1-onto→On → (∃𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 ¬ 𝑣𝑅𝑢 ↔ ∃𝑢 ∈ 𝑡 ∀𝑠 ∈ (𝐹 “ 𝑡)(𝐹‘𝑢) ⊆ 𝑠))
39		sseq1 3965	. . . . . . . . 9 ⊢ (𝑟 = (𝐹‘𝑢) → (𝑟 ⊆ 𝑠 ↔ (𝐹‘𝑢) ⊆ 𝑠))
40	39	ralbidv 3191	. . . . . . . 8 ⊢ (𝑟 = (𝐹‘𝑢) → (∀𝑠 ∈ (𝐹 “ 𝑡)𝑟 ⊆ 𝑠 ↔ ∀𝑠 ∈ (𝐹 “ 𝑡)(𝐹‘𝑢) ⊆ 𝑠))
41	40	rexima 7243	. . . . . . 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 5619	. . . 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 7086	. . . . . . . 8 ⊢ ((𝐹:V–1-1-onto→On ∧ 𝑤 ∈ V) → (𝐹‘𝑤) ∈ On)
53	52	elvd 3464	. . . . . . 7 ⊢ (𝐹:V–1-1-onto→On → (𝐹‘𝑤) ∈ On)
54	1	ffvelcdmda 7086	. . . . . . . 8 ⊢ ((𝐹:V–1-1-onto→On ∧ 𝑧 ∈ V) → (𝐹‘𝑧) ∈ On)
55	54	elvd 3464	. . . . . . 7 ⊢ (𝐹:V–1-1-onto→On → (𝐹‘𝑧) ∈ On)
56		oneltri 6411	. . . . . . 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 3462	. . . . . . . . 9 ⊢ 𝑤 ∈ V
61		vex 3462	. . . . . . . . 9 ⊢ 𝑧 ∈ V
62		fveq2 6888	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → (𝐹‘𝑥) = (𝐹‘𝑤))
63	62	eleq1d 2851	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → ((𝐹‘𝑥) ∈ (𝐹‘𝑦) ↔ (𝐹‘𝑤) ∈ (𝐹‘𝑦)))
64		fveq2 6888	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧))
65	64	eleq2d 2852	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ((𝐹‘𝑤) ∈ (𝐹‘𝑦) ↔ (𝐹‘𝑤) ∈ (𝐹‘𝑧)))
66	60, 61, 63, 65, 21	brab 5533	. . . . . . . 8 ⊢ (𝑤𝑅𝑧 ↔ (𝐹‘𝑤) ∈ (𝐹‘𝑧))
67	66	biimpri 231	. . . . . . 7 ⊢ ((𝐹‘𝑤) ∈ (𝐹‘𝑧) → 𝑤𝑅𝑧)
68	67	a1i 11	. . . . . 6 ⊢ (𝐹:V–1-1-onto→On → ((𝐹‘𝑤) ∈ (𝐹‘𝑧) → 𝑤𝑅𝑧))
69		f1of1 6826	. . . . . . 7 ⊢ (𝐹:V–1-1-onto→On → 𝐹:V–1-1→On)
70		f1veqaeq 7261	. . . . . . . 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 6888	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
74	73	eleq1d 2851	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) ∈ (𝐹‘𝑦) ↔ (𝐹‘𝑧) ∈ (𝐹‘𝑦)))
75		fveq2 6888	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → (𝐹‘𝑦) = (𝐹‘𝑤))
76	75	eleq2d 2852	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → ((𝐹‘𝑧) ∈ (𝐹‘𝑦) ↔ (𝐹‘𝑧) ∈ (𝐹‘𝑤)))
77	61, 60, 74, 76, 21	brab 5533	. . . . . . . 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 3164	. . 3 ⊢ (𝐹:V–1-1-onto→On → ∀𝑧 ∈ V (𝑤𝑅𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧𝑅𝑤))
83	82	ralrimivw 3164	. 2 ⊢ (𝐹:V–1-1-onto→On → ∀𝑤 ∈ V ∀𝑧 ∈ V (𝑤𝑅𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧𝑅𝑤))
84		dfwe2 7782	. 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 2146   ≠ wne 2961  ∀wral 3082  ∃wrex 3092  Vcvv 3458   ∩ cin 3907   ⊆ wss 3908  ∅c0 4289   class class class wbr 5114  {copab 5178   Fr wfr 5616   We wwe 5618  dom cdm 5666   “ cima 5669  Oncon0 6367   Fn wfn 6538  –1-1→wf1 6540  –1-1-onto→wf1o 6542  ‘cfv 6543

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409  ax-un 7745

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-tp 4599  df-op 4601  df-uni 4878  df-int 4918  df-br 5115  df-opab 5179  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-ord 6370  df-on 6371  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-f1o 6550  df-fv 6551

This theorem is used by: (None)