Theorem wessf1ornlem 43101

Description: Given a function 𝐹 on a well-ordered domain 𝐴 there exists a subset of 𝐴 such that 𝐹 restricted to such subset is injective and onto the range of 𝐹 (without using the axiom of choice). (Contributed by Glauco Siliprandi, 17-Aug-2020.)

Hypotheses

Ref	Expression
wessf1ornlem.f	⊢ (𝜑 → 𝐹 Fn 𝐴)
wessf1ornlem.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
wessf1ornlem.r	⊢ (𝜑 → 𝑅 We 𝐴)
wessf1ornlem.g	⊢ 𝐺 = (𝑦 ∈ ran 𝐹 ↦ (℩𝑥 ∈ (◡𝐹 “ {𝑦})∀𝑧 ∈ (◡𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥))

Assertion

Ref	Expression
wessf1ornlem	⊢ (𝜑 → ∃𝑥 ∈ 𝒫 𝐴(𝐹 ↾ 𝑥):𝑥–1-1-onto→ran 𝐹)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐹,𝑦,𝑧   𝑥,𝑅,𝑦,𝑧

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)   𝐴(𝑦,𝑧)   𝐺(𝑥,𝑦,𝑧)   𝑉(𝑥,𝑦,𝑧)

Proof of Theorem wessf1ornlem

Dummy variables 𝑡 𝑢 𝑣 𝑤 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		wessf1ornlem.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
2		cnvimass 6020	. . . . . . . 8 ⊢ (◡𝐹 “ {𝑢}) ⊆ dom 𝐹
3		wessf1ornlem.f	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 Fn 𝐴)
4	3	fndmd 6591	. . . . . . . . 9 ⊢ (𝜑 → dom 𝐹 = 𝐴)
5	4	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → dom 𝐹 = 𝐴)
6	2, 5	sseqtrid 3984	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (◡𝐹 “ {𝑢}) ⊆ 𝐴)
7		wessf1ornlem.r	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 We 𝐴)
8	7	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → 𝑅 We 𝐴)
9	2, 4	sseqtrid 3984	. . . . . . . . . . 11 ⊢ (𝜑 → (◡𝐹 “ {𝑢}) ⊆ 𝐴)
10	1, 9	ssexd 5269	. . . . . . . . . 10 ⊢ (𝜑 → (◡𝐹 “ {𝑢}) ∈ V)
11	10	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (◡𝐹 “ {𝑢}) ∈ V)
12		inisegn0 6037	. . . . . . . . . . 11 ⊢ (𝑢 ∈ ran 𝐹 ↔ (◡𝐹 “ {𝑢}) ≠ ∅)
13	12	biimpi 215	. . . . . . . . . 10 ⊢ (𝑢 ∈ ran 𝐹 → (◡𝐹 “ {𝑢}) ≠ ∅)
14	13	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (◡𝐹 “ {𝑢}) ≠ ∅)
15		wereu 5617	. . . . . . . . 9 ⊢ ((𝑅 We 𝐴 ∧ ((◡𝐹 “ {𝑢}) ∈ V ∧ (◡𝐹 “ {𝑢}) ⊆ 𝐴 ∧ (◡𝐹 “ {𝑢}) ≠ ∅)) → ∃!𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)
16	8, 11, 6, 14, 15	syl13anc 1371	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → ∃!𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)
17		riotacl 7312	. . . . . . . 8 ⊢ (∃!𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣 → (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ (◡𝐹 “ {𝑢}))
18	16, 17	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ (◡𝐹 “ {𝑢}))
19	6, 18	sseldd 3933	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ 𝐴)
20	19	ralrimiva 3139	. . . . 5 ⊢ (𝜑 → ∀𝑢 ∈ ran 𝐹(℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ 𝐴)
21		wessf1ornlem.g	. . . . . . 7 ⊢ 𝐺 = (𝑦 ∈ ran 𝐹 ↦ (℩𝑥 ∈ (◡𝐹 “ {𝑦})∀𝑧 ∈ (◡𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥))
22		sneq 4584	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑢 → {𝑦} = {𝑢})
23	22	imaeq2d 6000	. . . . . . . . . 10 ⊢ (𝑦 = 𝑢 → (◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑢}))
24	23	raleqdv 3309	. . . . . . . . . 10 ⊢ (𝑦 = 𝑢 → (∀𝑧 ∈ (◡𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥 ↔ ∀𝑧 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥))
25	23, 24	riotaeqbidv 7297	. . . . . . . . 9 ⊢ (𝑦 = 𝑢 → (℩𝑥 ∈ (◡𝐹 “ {𝑦})∀𝑧 ∈ (◡𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥) = (℩𝑥 ∈ (◡𝐹 “ {𝑢})∀𝑧 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥))
26		breq1 5096	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑡 → (𝑧𝑅𝑥 ↔ 𝑡𝑅𝑥))
27	26	notbid 317	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑡 → (¬ 𝑧𝑅𝑥 ↔ ¬ 𝑡𝑅𝑥))
28	27	cbvralvw 3221	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥 ↔ ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑥)
29		breq2 5097	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑣 → (𝑡𝑅𝑥 ↔ 𝑡𝑅𝑣))
30	29	notbid 317	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑣 → (¬ 𝑡𝑅𝑥 ↔ ¬ 𝑡𝑅𝑣))
31	30	ralbidv 3170	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑣 → (∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑥 ↔ ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
32	28, 31	bitrid 282	. . . . . . . . . 10 ⊢ (𝑥 = 𝑣 → (∀𝑧 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥 ↔ ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
33	32	cbvriotavw 7304	. . . . . . . . 9 ⊢ (℩𝑥 ∈ (◡𝐹 “ {𝑢})∀𝑧 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥) = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)
34	25, 33	eqtrdi 2792	. . . . . . . 8 ⊢ (𝑦 = 𝑢 → (℩𝑥 ∈ (◡𝐹 “ {𝑦})∀𝑧 ∈ (◡𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥) = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
35	34	cbvmptv 5206	. . . . . . 7 ⊢ (𝑦 ∈ ran 𝐹 ↦ (℩𝑥 ∈ (◡𝐹 “ {𝑦})∀𝑧 ∈ (◡𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥)) = (𝑢 ∈ ran 𝐹 ↦ (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
36	21, 35	eqtri 2764	. . . . . 6 ⊢ 𝐺 = (𝑢 ∈ ran 𝐹 ↦ (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
37	36	rnmptss 7053	. . . . 5 ⊢ (∀𝑢 ∈ ran 𝐹(℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ 𝐴 → ran 𝐺 ⊆ 𝐴)
38	20, 37	syl 17	. . . 4 ⊢ (𝜑 → ran 𝐺 ⊆ 𝐴)
39	1, 38	sselpwd 5271	. . 3 ⊢ (𝜑 → ran 𝐺 ∈ 𝒫 𝐴)
40		dffn3 6665	. . . . . . 7 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹)
41	3, 40	sylib 217	. . . . . 6 ⊢ (𝜑 → 𝐹:𝐴⟶ran 𝐹)
42	41, 38	fssresd 6693	. . . . 5 ⊢ (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺⟶ran 𝐹)
43		fvres 6845	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ ran 𝐺 → ((𝐹 ↾ ran 𝐺)‘𝑤) = (𝐹‘𝑤))
44	43	eqcomd 2742	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ ran 𝐺 → (𝐹‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑤))
45	44	ad2antrr 723	. . . . . . . . . . 11 ⊢ (((𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → (𝐹‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑤))
46		simpr 485	. . . . . . . . . . 11 ⊢ (((𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡))
47		fvres 6845	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ ran 𝐺 → ((𝐹 ↾ ran 𝐺)‘𝑡) = (𝐹‘𝑡))
48	47	ad2antlr 724	. . . . . . . . . . 11 ⊢ (((𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → ((𝐹 ↾ ran 𝐺)‘𝑡) = (𝐹‘𝑡))
49	45, 46, 48	3eqtrd 2780	. . . . . . . . . 10 ⊢ (((𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → (𝐹‘𝑤) = (𝐹‘𝑡))
50	49	3adantl1 1165	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → (𝐹‘𝑤) = (𝐹‘𝑡))
51		simpl1 1190	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → 𝜑)
52		simpl3 1192	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → 𝑡 ∈ ran 𝐺)
53		simpl2 1191	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → 𝑤 ∈ ran 𝐺)
54		id 22	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑤) = (𝐹‘𝑡) → (𝐹‘𝑤) = (𝐹‘𝑡))
55	54	eqcomd 2742	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑤) = (𝐹‘𝑡) → (𝐹‘𝑡) = (𝐹‘𝑤))
56	55	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → (𝐹‘𝑡) = (𝐹‘𝑤))
57		eleq1w 2819	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑤 → (𝑏 ∈ ran 𝐺 ↔ 𝑤 ∈ ran 𝐺))
58	57	3anbi3d 1441	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑤 → ((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ↔ (𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑤 ∈ ran 𝐺)))
59		fveq2 6826	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑤 → (𝐹‘𝑏) = (𝐹‘𝑤))
60	59	eqeq2d 2747	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑤 → ((𝐹‘𝑡) = (𝐹‘𝑏) ↔ (𝐹‘𝑡) = (𝐹‘𝑤)))
61	58, 60	anbi12d 631	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑤 → (((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑏)) ↔ ((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑤 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑤))))
62		breq1 5096	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑤 → (𝑏𝑅𝑡 ↔ 𝑤𝑅𝑡))
63	62	notbid 317	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑤 → (¬ 𝑏𝑅𝑡 ↔ ¬ 𝑤𝑅𝑡))
64	61, 63	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑤 → ((((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑏)) → ¬ 𝑏𝑅𝑡) ↔ (((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑤 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑤)) → ¬ 𝑤𝑅𝑡)))
65		eleq1w 2819	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑡 → (𝑎 ∈ ran 𝐺 ↔ 𝑡 ∈ ran 𝐺))
66	65	3anbi2d 1440	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑡 → ((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ↔ (𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺)))
67		fveqeq2 6835	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑡 → ((𝐹‘𝑎) = (𝐹‘𝑏) ↔ (𝐹‘𝑡) = (𝐹‘𝑏)))
68	66, 67	anbi12d 631	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑡 → (((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ↔ ((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑏))))
69		breq2 5097	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑡 → (𝑏𝑅𝑎 ↔ 𝑏𝑅𝑡))
70	69	notbid 317	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑡 → (¬ 𝑏𝑅𝑎 ↔ ¬ 𝑏𝑅𝑡))
71	68, 70	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑡 → ((((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ¬ 𝑏𝑅𝑎) ↔ (((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑏)) → ¬ 𝑏𝑅𝑡)))
72		eleq1w 2819	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑏 → (𝑡 ∈ ran 𝐺 ↔ 𝑏 ∈ ran 𝐺))
73	72	3anbi3d 1441	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑏 → ((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ↔ (𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺)))
74		fveq2 6826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑏 → (𝐹‘𝑡) = (𝐹‘𝑏))
75	74	eqeq2d 2747	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑏 → ((𝐹‘𝑎) = (𝐹‘𝑡) ↔ (𝐹‘𝑎) = (𝐹‘𝑏)))
76	73, 75	anbi12d 631	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑏 → (((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑡)) ↔ ((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑏))))
77		breq1 5096	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑏 → (𝑡𝑅𝑎 ↔ 𝑏𝑅𝑎))
78	77	notbid 317	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑏 → (¬ 𝑡𝑅𝑎 ↔ ¬ 𝑏𝑅𝑎))
79	76, 78	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑏 → ((((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑡)) → ¬ 𝑡𝑅𝑎) ↔ (((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ¬ 𝑏𝑅𝑎)))
80		eleq1w 2819	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑎 → (𝑤 ∈ ran 𝐺 ↔ 𝑎 ∈ ran 𝐺))
81	80	3anbi2d 1440	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑎 → ((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ↔ (𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺)))
82		fveqeq2 6835	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑎 → ((𝐹‘𝑤) = (𝐹‘𝑡) ↔ (𝐹‘𝑎) = (𝐹‘𝑡)))
83	81, 82	anbi12d 631	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑎 → (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ↔ ((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑡))))
84		breq2 5097	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑎 → (𝑡𝑅𝑤 ↔ 𝑡𝑅𝑎))
85	84	notbid 317	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑎 → (¬ 𝑡𝑅𝑤 ↔ ¬ 𝑡𝑅𝑎))
86	83, 85	imbi12d 344	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑎 → ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → ¬ 𝑡𝑅𝑤) ↔ (((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑡)) → ¬ 𝑡𝑅𝑎)))
87	36	elrnmpt 5898	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ V → (𝑤 ∈ ran 𝐺 ↔ ∃𝑢 ∈ ran 𝐹 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)))
88	87	elv 3447	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ ran 𝐺 ↔ ∃𝑢 ∈ ran 𝐹 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
89	88	biimpi 215	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ran 𝐺 → ∃𝑢 ∈ ran 𝐹 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
90	89	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 ∈ ran 𝐺 ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → ∃𝑢 ∈ ran 𝐹 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
91	90	3ad2antl2 1185	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → ∃𝑢 ∈ ran 𝐹 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
92		simp3 1137	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
93	92	eqcomd 2742	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = 𝑤)
94		simp11 1202	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝜑)
95		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
96		breq2 5097	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑣 = 𝑤 → (𝑡𝑅𝑣 ↔ 𝑡𝑅𝑤))
97	96	notbid 317	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑣 = 𝑤 → (¬ 𝑡𝑅𝑣 ↔ ¬ 𝑡𝑅𝑤))
98	97	ralbidv 3170	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑣 = 𝑤 → (∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣 ↔ ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤))
99	98	cbvriotavw 7304	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = (℩𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
100	95, 99	eqtr2di 2793	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → (℩𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤)
101	100	3ad2ant3 1134	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (℩𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤)
102	98	cbvreuvw 3373	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∃!𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣 ↔ ∃!𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
103	16, 102	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → ∃!𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
104		riota1 7316	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃!𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤 → ((𝑤 ∈ (◡𝐹 “ {𝑢}) ∧ ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) ↔ (℩𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤))
105	103, 104	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → ((𝑤 ∈ (◡𝐹 “ {𝑢}) ∧ ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) ↔ (℩𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤))
106	105	3adant3 1131	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ((𝑤 ∈ (◡𝐹 “ {𝑢}) ∧ ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) ↔ (℩𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤))
107	101, 106	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑤 ∈ (◡𝐹 “ {𝑢}) ∧ ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤))
108	107	simpld 495	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑤 ∈ (◡𝐹 “ {𝑢}))
109	94, 108	syld3an1 1409	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑤 ∈ (◡𝐹 “ {𝑢}))
110		simp2 1136	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑢 ∈ ran 𝐹)
111	94, 110, 16	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ∃!𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)
112	98	riota2 7320	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑤 ∈ (◡𝐹 “ {𝑢}) ∧ ∃!𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → (∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤 ↔ (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = 𝑤))
113	109, 111, 112	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤 ↔ (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = 𝑤))
114	93, 113	mpbird 256	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
115	114	3adant1r 1176	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
116	38	sselda 3932	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 ∈ ran 𝐺) → 𝑡 ∈ 𝐴)
117	116	3adant2 1130	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) → 𝑡 ∈ 𝐴)
118	117	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → 𝑡 ∈ 𝐴)
119	118	3ad2ant1 1132	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑡 ∈ 𝐴)
120	55	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹) → (𝐹‘𝑡) = (𝐹‘𝑤))
121	120	3adant3 1131	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝐹‘𝑡) = (𝐹‘𝑤))
122		fniniseg 6994	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹 Fn 𝐴 → (𝑤 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑤 ∈ 𝐴 ∧ (𝐹‘𝑤) = 𝑢)))
123	94, 3, 122	3syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑤 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑤 ∈ 𝐴 ∧ (𝐹‘𝑤) = 𝑢)))
124	109, 123	mpbid 231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑤 ∈ 𝐴 ∧ (𝐹‘𝑤) = 𝑢))
125	124	simprd 496	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝐹‘𝑤) = 𝑢)
126	125	3adant1r 1176	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝐹‘𝑤) = 𝑢)
127	121, 126	eqtrd 2776	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝐹‘𝑡) = 𝑢)
128		fniniseg 6994	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 Fn 𝐴 → (𝑡 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑡 ∈ 𝐴 ∧ (𝐹‘𝑡) = 𝑢)))
129	3, 128	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑡 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑡 ∈ 𝐴 ∧ (𝐹‘𝑡) = 𝑢)))
130	129	3ad2ant1 1132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) → (𝑡 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑡 ∈ 𝐴 ∧ (𝐹‘𝑡) = 𝑢)))
131	130	ad2antrr 723	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹) → (𝑡 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑡 ∈ 𝐴 ∧ (𝐹‘𝑡) = 𝑢)))
132	131	3adant3 1131	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑡 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑡 ∈ 𝐴 ∧ (𝐹‘𝑡) = 𝑢)))
133	119, 127, 132	mpbir2and 710	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑡 ∈ (◡𝐹 “ {𝑢}))
134		rspa 3227	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤 ∧ 𝑡 ∈ (◡𝐹 “ {𝑢})) → ¬ 𝑡𝑅𝑤)
135	115, 133, 134	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ¬ 𝑡𝑅𝑤)
136	135	rexlimdv3a 3152	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → (∃𝑢 ∈ ran 𝐹 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → ¬ 𝑡𝑅𝑤))
137	91, 136	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → ¬ 𝑡𝑅𝑤)
138	86, 137	chvarvv 2001	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑡)) → ¬ 𝑡𝑅𝑎)
139	79, 138	chvarvv 2001	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ¬ 𝑏𝑅𝑎)
140	71, 139	chvarvv 2001	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑏)) → ¬ 𝑏𝑅𝑡)
141	64, 140	chvarvv 2001	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑤 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑤)) → ¬ 𝑤𝑅𝑡)
142	51, 52, 53, 56, 141	syl31anc 1372	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → ¬ 𝑤𝑅𝑡)
143		weso 5612	. . . . . . . . . . . . . 14 ⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴)
144	7, 143	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 Or 𝐴)
145	144	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → 𝑅 Or 𝐴)
146	145	3ad2antl1 1184	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → 𝑅 Or 𝐴)
147	38	sselda 3932	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐺) → 𝑤 ∈ 𝐴)
148	147	3adant3 1131	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) → 𝑤 ∈ 𝐴)
149	148	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → 𝑤 ∈ 𝐴)
150		sotrieq2 5563	. . . . . . . . . . 11 ⊢ ((𝑅 Or 𝐴 ∧ (𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴)) → (𝑤 = 𝑡 ↔ (¬ 𝑤𝑅𝑡 ∧ ¬ 𝑡𝑅𝑤)))
151	146, 149, 118, 150	syl12anc 834	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → (𝑤 = 𝑡 ↔ (¬ 𝑤𝑅𝑡 ∧ ¬ 𝑡𝑅𝑤)))
152	142, 137, 151	mpbir2and 710	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → 𝑤 = 𝑡)
153	50, 152	syldan 591	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → 𝑤 = 𝑡)
154	153	ex 413	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) → (((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡))
155	154	3expb 1119	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺)) → (((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡))
156	155	ralrimivva 3193	. . . . 5 ⊢ (𝜑 → ∀𝑤 ∈ ran 𝐺∀𝑡 ∈ ran 𝐺(((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡))
157		dff13 7185	. . . . 5 ⊢ ((𝐹 ↾ ran 𝐺):ran 𝐺–1-1→ran 𝐹 ↔ ((𝐹 ↾ ran 𝐺):ran 𝐺⟶ran 𝐹 ∧ ∀𝑤 ∈ ran 𝐺∀𝑡 ∈ ran 𝐺(((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡)))
158	42, 156, 157	sylanbrc 583	. . . 4 ⊢ (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺–1-1→ran 𝐹)
159		riotaex 7298	. . . . . . . . . . 11 ⊢ (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V
160	159	rgenw 3065	. . . . . . . . . 10 ⊢ ∀𝑢 ∈ ran 𝐹(℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V
161	36	fnmpt 6625	. . . . . . . . . 10 ⊢ (∀𝑢 ∈ ran 𝐹(℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V → 𝐺 Fn ran 𝐹)
162	160, 161	mp1i 13	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 Fn ran 𝐹)
163		dffn3 6665	. . . . . . . . 9 ⊢ (𝐺 Fn ran 𝐹 ↔ 𝐺:ran 𝐹⟶ran 𝐺)
164	162, 163	sylib 217	. . . . . . . 8 ⊢ (𝜑 → 𝐺:ran 𝐹⟶ran 𝐺)
165	164	ffvelcdmda 7018	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (𝐺‘𝑢) ∈ ran 𝐺)
166	165	fvresd 6846	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → ((𝐹 ↾ ran 𝐺)‘(𝐺‘𝑢)) = (𝐹‘(𝐺‘𝑢)))
167		simpr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → 𝑢 ∈ ran 𝐹)
168	159	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V)
169	21, 34, 167, 168	fvmptd3 6955	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (𝐺‘𝑢) = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
170	169, 18	eqeltrd 2837	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (𝐺‘𝑢) ∈ (◡𝐹 “ {𝑢}))
171		fvex 6839	. . . . . . . . . . . 12 ⊢ (𝐺‘𝑢) ∈ V
172		eleq1 2824	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝐺‘𝑢) → (𝑤 ∈ (◡𝐹 “ {𝑢}) ↔ (𝐺‘𝑢) ∈ (◡𝐹 “ {𝑢})))
173		eleq1 2824	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝐺‘𝑢) → (𝑤 ∈ 𝐴 ↔ (𝐺‘𝑢) ∈ 𝐴))
174		fveqeq2 6835	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝐺‘𝑢) → ((𝐹‘𝑤) = 𝑢 ↔ (𝐹‘(𝐺‘𝑢)) = 𝑢))
175	173, 174	anbi12d 631	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝐺‘𝑢) → ((𝑤 ∈ 𝐴 ∧ (𝐹‘𝑤) = 𝑢) ↔ ((𝐺‘𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝑢)) = 𝑢)))
176	172, 175	bibi12d 345	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝐺‘𝑢) → ((𝑤 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑤 ∈ 𝐴 ∧ (𝐹‘𝑤) = 𝑢)) ↔ ((𝐺‘𝑢) ∈ (◡𝐹 “ {𝑢}) ↔ ((𝐺‘𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝑢)) = 𝑢))))
177	176	imbi2d 340	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝐺‘𝑢) → ((𝜑 → (𝑤 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑤 ∈ 𝐴 ∧ (𝐹‘𝑤) = 𝑢))) ↔ (𝜑 → ((𝐺‘𝑢) ∈ (◡𝐹 “ {𝑢}) ↔ ((𝐺‘𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝑢)) = 𝑢)))))
178	3, 122	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑤 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑤 ∈ 𝐴 ∧ (𝐹‘𝑤) = 𝑢)))
179	171, 177, 178	vtocl 3507	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐺‘𝑢) ∈ (◡𝐹 “ {𝑢}) ↔ ((𝐺‘𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝑢)) = 𝑢)))
180	179	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → ((𝐺‘𝑢) ∈ (◡𝐹 “ {𝑢}) ↔ ((𝐺‘𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝑢)) = 𝑢)))
181	170, 180	mpbid 231	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → ((𝐺‘𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝑢)) = 𝑢))
182	181	simprd 496	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (𝐹‘(𝐺‘𝑢)) = 𝑢)
183	166, 182	eqtr2d 2777	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → 𝑢 = ((𝐹 ↾ ran 𝐺)‘(𝐺‘𝑢)))
184		fveq2 6826	. . . . . . . 8 ⊢ (𝑤 = (𝐺‘𝑢) → ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘(𝐺‘𝑢)))
185	184	rspceeqv 3584	. . . . . . 7 ⊢ (((𝐺‘𝑢) ∈ ran 𝐺 ∧ 𝑢 = ((𝐹 ↾ ran 𝐺)‘(𝐺‘𝑢))) → ∃𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤))
186	165, 183, 185	syl2anc 584	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → ∃𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤))
187	186	ralrimiva 3139	. . . . 5 ⊢ (𝜑 → ∀𝑢 ∈ ran 𝐹∃𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤))
188		dffo3 7035	. . . . 5 ⊢ ((𝐹 ↾ ran 𝐺):ran 𝐺–onto→ran 𝐹 ↔ ((𝐹 ↾ ran 𝐺):ran 𝐺⟶ran 𝐹 ∧ ∀𝑢 ∈ ran 𝐹∃𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤)))
189	42, 187, 188	sylanbrc 583	. . . 4 ⊢ (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺–onto→ran 𝐹)
190		df-f1o 6487	. . . 4 ⊢ ((𝐹 ↾ ran 𝐺):ran 𝐺–1-1-onto→ran 𝐹 ↔ ((𝐹 ↾ ran 𝐺):ran 𝐺–1-1→ran 𝐹 ∧ (𝐹 ↾ ran 𝐺):ran 𝐺–onto→ran 𝐹))
191	158, 189, 190	sylanbrc 583	. . 3 ⊢ (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺–1-1-onto→ran 𝐹)
192		reseq2 5919	. . . . 5 ⊢ (𝑣 = ran 𝐺 → (𝐹 ↾ 𝑣) = (𝐹 ↾ ran 𝐺))
193		id 22	. . . . 5 ⊢ (𝑣 = ran 𝐺 → 𝑣 = ran 𝐺)
194		eqidd 2737	. . . . 5 ⊢ (𝑣 = ran 𝐺 → ran 𝐹 = ran 𝐹)
195	192, 193, 194	f1oeq123d 6762	. . . 4 ⊢ (𝑣 = ran 𝐺 → ((𝐹 ↾ 𝑣):𝑣–1-1-onto→ran 𝐹 ↔ (𝐹 ↾ ran 𝐺):ran 𝐺–1-1-onto→ran 𝐹))
196	195	rspcev 3570	. . 3 ⊢ ((ran 𝐺 ∈ 𝒫 𝐴 ∧ (𝐹 ↾ ran 𝐺):ran 𝐺–1-1-onto→ran 𝐹) → ∃𝑣 ∈ 𝒫 𝐴(𝐹 ↾ 𝑣):𝑣–1-1-onto→ran 𝐹)
197	39, 191, 196	syl2anc 584	. 2 ⊢ (𝜑 → ∃𝑣 ∈ 𝒫 𝐴(𝐹 ↾ 𝑣):𝑣–1-1-onto→ran 𝐹)
198		reseq2 5919	. . . 4 ⊢ (𝑣 = 𝑥 → (𝐹 ↾ 𝑣) = (𝐹 ↾ 𝑥))
199		id 22	. . . 4 ⊢ (𝑣 = 𝑥 → 𝑣 = 𝑥)
200		eqidd 2737	. . . 4 ⊢ (𝑣 = 𝑥 → ran 𝐹 = ran 𝐹)
201	198, 199, 200	f1oeq123d 6762	. . 3 ⊢ (𝑣 = 𝑥 → ((𝐹 ↾ 𝑣):𝑣–1-1-onto→ran 𝐹 ↔ (𝐹 ↾ 𝑥):𝑥–1-1-onto→ran 𝐹))
202	201	cbvrexvw 3222	. 2 ⊢ (∃𝑣 ∈ 𝒫 𝐴(𝐹 ↾ 𝑣):𝑣–1-1-onto→ran 𝐹 ↔ ∃𝑥 ∈ 𝒫 𝐴(𝐹 ↾ 𝑥):𝑥–1-1-onto→ran 𝐹)
203	197, 202	sylib 217	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝒫 𝐴(𝐹 ↾ 𝑥):𝑥–1-1-onto→ran 𝐹)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105   ≠ wne 2940  ∀wral 3061  ∃wrex 3070  ∃!wreu 3347  Vcvv 3441   ⊆ wss 3898  ∅c0 4270  𝒫 cpw 4548  {csn 4574   class class class wbr 5093   ↦ cmpt 5176   Or wor 5532   We wwe 5575  ^◡ccnv 5620  dom cdm 5621  ran crn 5622   ↾ cres 5623   “ cima 5624   Fn wfn 6475  ⟶wf 6476  –1-1→wf1 6477  –onto→wfo 6478  –1-1-onto→wf1o 6479  ‘cfv 6480  ℩crio 7293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5244  ax-nul 5251  ax-pr 5373

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4271  df-if 4475  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4854  df-br 5094  df-opab 5156  df-mpt 5177  df-id 5519  df-po 5533  df-so 5534  df-fr 5576  df-we 5578  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6432  df-fun 6482  df-fn 6483  df-f 6484  df-f1 6485  df-fo 6486  df-f1o 6487  df-fv 6488  df-riota 7294

This theorem is referenced by:  wessf1orn  43102