Theorem wessf1ornlem 45636

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 6042	. . . . . . . 8 ⊢ (◡𝐹 “ {𝑢}) ⊆ dom 𝐹
3		wessf1ornlem.f	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 Fn 𝐴)
4	3	fndmd 6598	. . . . . . . . 9 ⊢ (𝜑 → dom 𝐹 = 𝐴)
5	4	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → dom 𝐹 = 𝐴)
6	2, 5	sseqtrid 3965	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (◡𝐹 “ {𝑢}) ⊆ 𝐴)
7		wessf1ornlem.r	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 We 𝐴)
8	7	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → 𝑅 We 𝐴)
9	2, 4	sseqtrid 3965	. . . . . . . . . . 11 ⊢ (𝜑 → (◡𝐹 “ {𝑢}) ⊆ 𝐴)
10	1, 9	ssexd 5262	. . . . . . . . . 10 ⊢ (𝜑 → (◡𝐹 “ {𝑢}) ∈ V)
11	10	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (◡𝐹 “ {𝑢}) ∈ V)
12		inisegn0 6058	. . . . . . . . . . 11 ⊢ (𝑢 ∈ ran 𝐹 ↔ (◡𝐹 “ {𝑢}) ≠ ∅)
13	12	biimpi 216	. . . . . . . . . 10 ⊢ (𝑢 ∈ ran 𝐹 → (◡𝐹 “ {𝑢}) ≠ ∅)
14	13	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (◡𝐹 “ {𝑢}) ≠ ∅)
15		wereu 5621	. . . . . . . . 9 ⊢ ((𝑅 We 𝐴 ∧ ((◡𝐹 “ {𝑢}) ∈ V ∧ (◡𝐹 “ {𝑢}) ⊆ 𝐴 ∧ (◡𝐹 “ {𝑢}) ≠ ∅)) → ∃!𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)
16	8, 11, 6, 14, 15	syl13anc 1375	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → ∃!𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)
17		riotacl 7335	. . . . . . . 8 ⊢ (∃!𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣 → (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ (◡𝐹 “ {𝑢}))
18	16, 17	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ (◡𝐹 “ {𝑢}))
19	6, 18	sseldd 3923	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ 𝐴)
20	19	ralrimiva 3130	. . . . 5 ⊢ (𝜑 → ∀𝑢 ∈ ran 𝐹(℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ 𝐴)
21		wessf1ornlem.g	. . . . . . 7 ⊢ 𝐺 = (𝑦 ∈ ran 𝐹 ↦ (℩𝑥 ∈ (◡𝐹 “ {𝑦})∀𝑧 ∈ (◡𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥))
22		sneq 4578	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑢 → {𝑦} = {𝑢})
23	22	imaeq2d 6020	. . . . . . . . . 10 ⊢ (𝑦 = 𝑢 → (◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑢}))
24	23	raleqdv 3296	. . . . . . . . . 10 ⊢ (𝑦 = 𝑢 → (∀𝑧 ∈ (◡𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥 ↔ ∀𝑧 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥))
25	23, 24	riotaeqbidv 7321	. . . . . . . . 9 ⊢ (𝑦 = 𝑢 → (℩𝑥 ∈ (◡𝐹 “ {𝑦})∀𝑧 ∈ (◡𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥) = (℩𝑥 ∈ (◡𝐹 “ {𝑢})∀𝑧 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥))
26		breq1 5089	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑡 → (𝑧𝑅𝑥 ↔ 𝑡𝑅𝑥))
27	26	notbid 318	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑡 → (¬ 𝑧𝑅𝑥 ↔ ¬ 𝑡𝑅𝑥))
28	27	cbvralvw 3216	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥 ↔ ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑥)
29		breq2 5090	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑣 → (𝑡𝑅𝑥 ↔ 𝑡𝑅𝑣))
30	29	notbid 318	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑣 → (¬ 𝑡𝑅𝑥 ↔ ¬ 𝑡𝑅𝑣))
31	30	ralbidv 3161	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑣 → (∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑥 ↔ ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
32	28, 31	bitrid 283	. . . . . . . . . 10 ⊢ (𝑥 = 𝑣 → (∀𝑧 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥 ↔ ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
33	32	cbvriotavw 7328	. . . . . . . . 9 ⊢ (℩𝑥 ∈ (◡𝐹 “ {𝑢})∀𝑧 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥) = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)
34	25, 33	eqtrdi 2788	. . . . . . . 8 ⊢ (𝑦 = 𝑢 → (℩𝑥 ∈ (◡𝐹 “ {𝑦})∀𝑧 ∈ (◡𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥) = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
35	34	cbvmptv 5190	. . . . . . 7 ⊢ (𝑦 ∈ ran 𝐹 ↦ (℩𝑥 ∈ (◡𝐹 “ {𝑦})∀𝑧 ∈ (◡𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥)) = (𝑢 ∈ ran 𝐹 ↦ (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
36	21, 35	eqtri 2760	. . . . . 6 ⊢ 𝐺 = (𝑢 ∈ ran 𝐹 ↦ (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
37	36	rnmptss 7070	. . . . 5 ⊢ (∀𝑢 ∈ ran 𝐹(℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ 𝐴 → ran 𝐺 ⊆ 𝐴)
38	20, 37	syl 17	. . . 4 ⊢ (𝜑 → ran 𝐺 ⊆ 𝐴)
39	1, 38	sselpwd 5266	. . 3 ⊢ (𝜑 → ran 𝐺 ∈ 𝒫 𝐴)
40		dffn3 6675	. . . . . . 7 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹)
41	3, 40	sylib 218	. . . . . 6 ⊢ (𝜑 → 𝐹:𝐴⟶ran 𝐹)
42	41, 38	fssresd 6702	. . . . 5 ⊢ (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺⟶ran 𝐹)
43		fvres 6854	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ ran 𝐺 → ((𝐹 ↾ ran 𝐺)‘𝑤) = (𝐹‘𝑤))
44	43	eqcomd 2743	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ ran 𝐺 → (𝐹‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑤))
45	44	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → (𝐹‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑤))
46		simpr 484	. . . . . . . . . . 11 ⊢ (((𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡))
47		fvres 6854	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ ran 𝐺 → ((𝐹 ↾ ran 𝐺)‘𝑡) = (𝐹‘𝑡))
48	47	ad2antlr 728	. . . . . . . . . . 11 ⊢ (((𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → ((𝐹 ↾ ran 𝐺)‘𝑡) = (𝐹‘𝑡))
49	45, 46, 48	3eqtrd 2776	. . . . . . . . . 10 ⊢ (((𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → (𝐹‘𝑤) = (𝐹‘𝑡))
50	49	3adantl1 1168	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → (𝐹‘𝑤) = (𝐹‘𝑡))
51		simpl1 1193	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → 𝜑)
52		simpl3 1195	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → 𝑡 ∈ ran 𝐺)
53		simpl2 1194	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → 𝑤 ∈ ran 𝐺)
54		id 22	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑤) = (𝐹‘𝑡) → (𝐹‘𝑤) = (𝐹‘𝑡))
55	54	eqcomd 2743	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑤) = (𝐹‘𝑡) → (𝐹‘𝑡) = (𝐹‘𝑤))
56	55	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → (𝐹‘𝑡) = (𝐹‘𝑤))
57		eleq1w 2820	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑤 → (𝑏 ∈ ran 𝐺 ↔ 𝑤 ∈ ran 𝐺))
58	57	3anbi3d 1445	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑤 → ((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ↔ (𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑤 ∈ ran 𝐺)))
59		fveq2 6835	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑤 → (𝐹‘𝑏) = (𝐹‘𝑤))
60	59	eqeq2d 2748	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑤 → ((𝐹‘𝑡) = (𝐹‘𝑏) ↔ (𝐹‘𝑡) = (𝐹‘𝑤)))
61	58, 60	anbi12d 633	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑤 → (((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑏)) ↔ ((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑤 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑤))))
62		breq1 5089	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑤 → (𝑏𝑅𝑡 ↔ 𝑤𝑅𝑡))
63	62	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑤 → (¬ 𝑏𝑅𝑡 ↔ ¬ 𝑤𝑅𝑡))
64	61, 63	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑤 → ((((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑏)) → ¬ 𝑏𝑅𝑡) ↔ (((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑤 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑤)) → ¬ 𝑤𝑅𝑡)))
65		eleq1w 2820	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑡 → (𝑎 ∈ ran 𝐺 ↔ 𝑡 ∈ ran 𝐺))
66	65	3anbi2d 1444	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑡 → ((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ↔ (𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺)))
67		fveqeq2 6844	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑡 → ((𝐹‘𝑎) = (𝐹‘𝑏) ↔ (𝐹‘𝑡) = (𝐹‘𝑏)))
68	66, 67	anbi12d 633	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑡 → (((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ↔ ((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑏))))
69		breq2 5090	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑡 → (𝑏𝑅𝑎 ↔ 𝑏𝑅𝑡))
70	69	notbid 318	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑡 → (¬ 𝑏𝑅𝑎 ↔ ¬ 𝑏𝑅𝑡))
71	68, 70	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑡 → ((((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ¬ 𝑏𝑅𝑎) ↔ (((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑏)) → ¬ 𝑏𝑅𝑡)))
72		eleq1w 2820	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑏 → (𝑡 ∈ ran 𝐺 ↔ 𝑏 ∈ ran 𝐺))
73	72	3anbi3d 1445	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑏 → ((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ↔ (𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺)))
74		fveq2 6835	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑏 → (𝐹‘𝑡) = (𝐹‘𝑏))
75	74	eqeq2d 2748	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑏 → ((𝐹‘𝑎) = (𝐹‘𝑡) ↔ (𝐹‘𝑎) = (𝐹‘𝑏)))
76	73, 75	anbi12d 633	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑏 → (((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑡)) ↔ ((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑏))))
77		breq1 5089	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑏 → (𝑡𝑅𝑎 ↔ 𝑏𝑅𝑎))
78	77	notbid 318	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑏 → (¬ 𝑡𝑅𝑎 ↔ ¬ 𝑏𝑅𝑎))
79	76, 78	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑏 → ((((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑡)) → ¬ 𝑡𝑅𝑎) ↔ (((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ¬ 𝑏𝑅𝑎)))
80		eleq1w 2820	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑎 → (𝑤 ∈ ran 𝐺 ↔ 𝑎 ∈ ran 𝐺))
81	80	3anbi2d 1444	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑎 → ((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ↔ (𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺)))
82		fveqeq2 6844	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑎 → ((𝐹‘𝑤) = (𝐹‘𝑡) ↔ (𝐹‘𝑎) = (𝐹‘𝑡)))
83	81, 82	anbi12d 633	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑎 → (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ↔ ((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑡))))
84		breq2 5090	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑎 → (𝑡𝑅𝑤 ↔ 𝑡𝑅𝑎))
85	84	notbid 318	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑎 → (¬ 𝑡𝑅𝑤 ↔ ¬ 𝑡𝑅𝑎))
86	83, 85	imbi12d 344	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑎 → ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → ¬ 𝑡𝑅𝑤) ↔ (((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑡)) → ¬ 𝑡𝑅𝑎)))
87	36	elrnmpt 5908	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ V → (𝑤 ∈ ran 𝐺 ↔ ∃𝑢 ∈ ran 𝐹 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)))
88	87	elv 3435	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ ran 𝐺 ↔ ∃𝑢 ∈ ran 𝐹 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
89	88	biimpi 216	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ran 𝐺 → ∃𝑢 ∈ ran 𝐹 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
90	89	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 ∈ ran 𝐺 ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → ∃𝑢 ∈ ran 𝐹 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
91	90	3ad2antl2 1188	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → ∃𝑢 ∈ ran 𝐹 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
92		simp3 1139	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
93	92	eqcomd 2743	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = 𝑤)
94		simp11 1205	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝜑)
95		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
96		breq2 5090	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑣 = 𝑤 → (𝑡𝑅𝑣 ↔ 𝑡𝑅𝑤))
97	96	notbid 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑣 = 𝑤 → (¬ 𝑡𝑅𝑣 ↔ ¬ 𝑡𝑅𝑤))
98	97	ralbidv 3161	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑣 = 𝑤 → (∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣 ↔ ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤))
99	98	cbvriotavw 7328	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = (℩𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
100	95, 99	eqtr2di 2789	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → (℩𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤)
101	100	3ad2ant3 1136	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (℩𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤)
102	98	cbvreuvw 3365	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∃!𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣 ↔ ∃!𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
103	16, 102	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → ∃!𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
104		riota1 7339	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃!𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤 → ((𝑤 ∈ (◡𝐹 “ {𝑢}) ∧ ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) ↔ (℩𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤))
105	103, 104	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → ((𝑤 ∈ (◡𝐹 “ {𝑢}) ∧ ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) ↔ (℩𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤))
106	105	3adant3 1133	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ((𝑤 ∈ (◡𝐹 “ {𝑢}) ∧ ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) ↔ (℩𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤))
107	101, 106	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑤 ∈ (◡𝐹 “ {𝑢}) ∧ ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤))
108	107	simpld 494	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑤 ∈ (◡𝐹 “ {𝑢}))
109	94, 108	syld3an1 1413	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑤 ∈ (◡𝐹 “ {𝑢}))
110		simp2 1138	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑢 ∈ ran 𝐹)
111	94, 110, 16	syl2anc 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ∃!𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)
112	98	riota2 7343	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑤 ∈ (◡𝐹 “ {𝑢}) ∧ ∃!𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → (∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤 ↔ (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = 𝑤))
113	109, 111, 112	syl2anc 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤 ↔ (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = 𝑤))
114	93, 113	mpbird 257	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
115	114	3adant1r 1179	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
116	38	sselda 3922	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 ∈ ran 𝐺) → 𝑡 ∈ 𝐴)
117	116	3adant2 1132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) → 𝑡 ∈ 𝐴)
118	117	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → 𝑡 ∈ 𝐴)
119	118	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑡 ∈ 𝐴)
120	55	ad2antlr 728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹) → (𝐹‘𝑡) = (𝐹‘𝑤))
121	120	3adant3 1133	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝐹‘𝑡) = (𝐹‘𝑤))
122		fniniseg 7007	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹 Fn 𝐴 → (𝑤 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑤 ∈ 𝐴 ∧ (𝐹‘𝑤) = 𝑢)))
123	94, 3, 122	3syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑤 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑤 ∈ 𝐴 ∧ (𝐹‘𝑤) = 𝑢)))
124	109, 123	mpbid 232	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑤 ∈ 𝐴 ∧ (𝐹‘𝑤) = 𝑢))
125	124	simprd 495	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝐹‘𝑤) = 𝑢)
126	125	3adant1r 1179	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝐹‘𝑤) = 𝑢)
127	121, 126	eqtrd 2772	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝐹‘𝑡) = 𝑢)
128		fniniseg 7007	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 Fn 𝐴 → (𝑡 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑡 ∈ 𝐴 ∧ (𝐹‘𝑡) = 𝑢)))
129	3, 128	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑡 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑡 ∈ 𝐴 ∧ (𝐹‘𝑡) = 𝑢)))
130	129	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) → (𝑡 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑡 ∈ 𝐴 ∧ (𝐹‘𝑡) = 𝑢)))
131	130	ad2antrr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹) → (𝑡 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑡 ∈ 𝐴 ∧ (𝐹‘𝑡) = 𝑢)))
132	131	3adant3 1133	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑡 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑡 ∈ 𝐴 ∧ (𝐹‘𝑡) = 𝑢)))
133	119, 127, 132	mpbir2and 714	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑡 ∈ (◡𝐹 “ {𝑢}))
134		rspa 3227	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤 ∧ 𝑡 ∈ (◡𝐹 “ {𝑢})) → ¬ 𝑡𝑅𝑤)
135	115, 133, 134	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ¬ 𝑡𝑅𝑤)
136	135	rexlimdv3a 3143	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → (∃𝑢 ∈ ran 𝐹 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → ¬ 𝑡𝑅𝑤))
137	91, 136	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → ¬ 𝑡𝑅𝑤)
138	86, 137	chvarvv 1991	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑡)) → ¬ 𝑡𝑅𝑎)
139	79, 138	chvarvv 1991	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ¬ 𝑏𝑅𝑎)
140	71, 139	chvarvv 1991	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑏)) → ¬ 𝑏𝑅𝑡)
141	64, 140	chvarvv 1991	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑤 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑤)) → ¬ 𝑤𝑅𝑡)
142	51, 52, 53, 56, 141	syl31anc 1376	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → ¬ 𝑤𝑅𝑡)
143		weso 5616	. . . . . . . . . . . . . 14 ⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴)
144	7, 143	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 Or 𝐴)
145	144	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → 𝑅 Or 𝐴)
146	145	3ad2antl1 1187	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → 𝑅 Or 𝐴)
147	38	sselda 3922	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐺) → 𝑤 ∈ 𝐴)
148	147	3adant3 1133	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) → 𝑤 ∈ 𝐴)
149	148	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → 𝑤 ∈ 𝐴)
150		sotrieq2 5565	. . . . . . . . . . 11 ⊢ ((𝑅 Or 𝐴 ∧ (𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴)) → (𝑤 = 𝑡 ↔ (¬ 𝑤𝑅𝑡 ∧ ¬ 𝑡𝑅𝑤)))
151	146, 149, 118, 150	syl12anc 837	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → (𝑤 = 𝑡 ↔ (¬ 𝑤𝑅𝑡 ∧ ¬ 𝑡𝑅𝑤)))
152	142, 137, 151	mpbir2and 714	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → 𝑤 = 𝑡)
153	50, 152	syldan 592	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → 𝑤 = 𝑡)
154	153	ex 412	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) → (((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡))
155	154	3expb 1121	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺)) → (((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡))
156	155	ralrimivva 3181	. . . . 5 ⊢ (𝜑 → ∀𝑤 ∈ ran 𝐺∀𝑡 ∈ ran 𝐺(((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡))
157		dff13 7203	. . . . 5 ⊢ ((𝐹 ↾ ran 𝐺):ran 𝐺–1-1→ran 𝐹 ↔ ((𝐹 ↾ ran 𝐺):ran 𝐺⟶ran 𝐹 ∧ ∀𝑤 ∈ ran 𝐺∀𝑡 ∈ ran 𝐺(((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡)))
158	42, 156, 157	sylanbrc 584	. . . 4 ⊢ (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺–1-1→ran 𝐹)
159		riotaex 7322	. . . . . . . . . . 11 ⊢ (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V
160	159	rgenw 3056	. . . . . . . . . 10 ⊢ ∀𝑢 ∈ ran 𝐹(℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V
161	36	fnmpt 6633	. . . . . . . . . 10 ⊢ (∀𝑢 ∈ ran 𝐹(℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V → 𝐺 Fn ran 𝐹)
162	160, 161	mp1i 13	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 Fn ran 𝐹)
163		dffn3 6675	. . . . . . . . 9 ⊢ (𝐺 Fn ran 𝐹 ↔ 𝐺:ran 𝐹⟶ran 𝐺)
164	162, 163	sylib 218	. . . . . . . 8 ⊢ (𝜑 → 𝐺:ran 𝐹⟶ran 𝐺)
165	164	ffvelcdmda 7031	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (𝐺‘𝑢) ∈ ran 𝐺)
166	165	fvresd 6855	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → ((𝐹 ↾ ran 𝐺)‘(𝐺‘𝑢)) = (𝐹‘(𝐺‘𝑢)))
167		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → 𝑢 ∈ ran 𝐹)
168	159	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V)
169	21, 34, 167, 168	fvmptd3 6966	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (𝐺‘𝑢) = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
170	169, 18	eqeltrd 2837	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (𝐺‘𝑢) ∈ (◡𝐹 “ {𝑢}))
171		fvex 6848	. . . . . . . . . . . 12 ⊢ (𝐺‘𝑢) ∈ V
172		eleq1 2825	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝐺‘𝑢) → (𝑤 ∈ (◡𝐹 “ {𝑢}) ↔ (𝐺‘𝑢) ∈ (◡𝐹 “ {𝑢})))
173		eleq1 2825	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝐺‘𝑢) → (𝑤 ∈ 𝐴 ↔ (𝐺‘𝑢) ∈ 𝐴))
174		fveqeq2 6844	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝐺‘𝑢) → ((𝐹‘𝑤) = 𝑢 ↔ (𝐹‘(𝐺‘𝑢)) = 𝑢))
175	173, 174	anbi12d 633	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝐺‘𝑢) → ((𝑤 ∈ 𝐴 ∧ (𝐹‘𝑤) = 𝑢) ↔ ((𝐺‘𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝑢)) = 𝑢)))
176	172, 175	bibi12d 345	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝐺‘𝑢) → ((𝑤 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑤 ∈ 𝐴 ∧ (𝐹‘𝑤) = 𝑢)) ↔ ((𝐺‘𝑢) ∈ (◡𝐹 “ {𝑢}) ↔ ((𝐺‘𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝑢)) = 𝑢))))
177	176	imbi2d 340	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝐺‘𝑢) → ((𝜑 → (𝑤 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑤 ∈ 𝐴 ∧ (𝐹‘𝑤) = 𝑢))) ↔ (𝜑 → ((𝐺‘𝑢) ∈ (◡𝐹 “ {𝑢}) ↔ ((𝐺‘𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝑢)) = 𝑢)))))
178	3, 122	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑤 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑤 ∈ 𝐴 ∧ (𝐹‘𝑤) = 𝑢)))
179	171, 177, 178	vtocl 3504	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐺‘𝑢) ∈ (◡𝐹 “ {𝑢}) ↔ ((𝐺‘𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝑢)) = 𝑢)))
180	179	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → ((𝐺‘𝑢) ∈ (◡𝐹 “ {𝑢}) ↔ ((𝐺‘𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝑢)) = 𝑢)))
181	170, 180	mpbid 232	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → ((𝐺‘𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝑢)) = 𝑢))
182	181	simprd 495	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (𝐹‘(𝐺‘𝑢)) = 𝑢)
183	166, 182	eqtr2d 2773	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → 𝑢 = ((𝐹 ↾ ran 𝐺)‘(𝐺‘𝑢)))
184		fveq2 6835	. . . . . . . 8 ⊢ (𝑤 = (𝐺‘𝑢) → ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘(𝐺‘𝑢)))
185	184	rspceeqv 3588	. . . . . . 7 ⊢ (((𝐺‘𝑢) ∈ ran 𝐺 ∧ 𝑢 = ((𝐹 ↾ ran 𝐺)‘(𝐺‘𝑢))) → ∃𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤))
186	165, 183, 185	syl2anc 585	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → ∃𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤))
187	186	ralrimiva 3130	. . . . 5 ⊢ (𝜑 → ∀𝑢 ∈ ran 𝐹∃𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤))
188		dffo3 7049	. . . . 5 ⊢ ((𝐹 ↾ ran 𝐺):ran 𝐺–onto→ran 𝐹 ↔ ((𝐹 ↾ ran 𝐺):ran 𝐺⟶ran 𝐹 ∧ ∀𝑢 ∈ ran 𝐹∃𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤)))
189	42, 187, 188	sylanbrc 584	. . . 4 ⊢ (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺–onto→ran 𝐹)
190		df-f1o 6500	. . . 4 ⊢ ((𝐹 ↾ ran 𝐺):ran 𝐺–1-1-onto→ran 𝐹 ↔ ((𝐹 ↾ ran 𝐺):ran 𝐺–1-1→ran 𝐹 ∧ (𝐹 ↾ ran 𝐺):ran 𝐺–onto→ran 𝐹))
191	158, 189, 190	sylanbrc 584	. . 3 ⊢ (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺–1-1-onto→ran 𝐹)
192		reseq2 5934	. . . . 5 ⊢ (𝑣 = ran 𝐺 → (𝐹 ↾ 𝑣) = (𝐹 ↾ ran 𝐺))
193		id 22	. . . . 5 ⊢ (𝑣 = ran 𝐺 → 𝑣 = ran 𝐺)
194		eqidd 2738	. . . . 5 ⊢ (𝑣 = ran 𝐺 → ran 𝐹 = ran 𝐹)
195	192, 193, 194	f1oeq123d 6769	. . . 4 ⊢ (𝑣 = ran 𝐺 → ((𝐹 ↾ 𝑣):𝑣–1-1-onto→ran 𝐹 ↔ (𝐹 ↾ ran 𝐺):ran 𝐺–1-1-onto→ran 𝐹))
196	195	rspcev 3565	. . 3 ⊢ ((ran 𝐺 ∈ 𝒫 𝐴 ∧ (𝐹 ↾ ran 𝐺):ran 𝐺–1-1-onto→ran 𝐹) → ∃𝑣 ∈ 𝒫 𝐴(𝐹 ↾ 𝑣):𝑣–1-1-onto→ran 𝐹)
197	39, 191, 196	syl2anc 585	. 2 ⊢ (𝜑 → ∃𝑣 ∈ 𝒫 𝐴(𝐹 ↾ 𝑣):𝑣–1-1-onto→ran 𝐹)
198		reseq2 5934	. . . 4 ⊢ (𝑣 = 𝑥 → (𝐹 ↾ 𝑣) = (𝐹 ↾ 𝑥))
199		id 22	. . . 4 ⊢ (𝑣 = 𝑥 → 𝑣 = 𝑥)
200		eqidd 2738	. . . 4 ⊢ (𝑣 = 𝑥 → ran 𝐹 = ran 𝐹)
201	198, 199, 200	f1oeq123d 6769	. . 3 ⊢ (𝑣 = 𝑥 → ((𝐹 ↾ 𝑣):𝑣–1-1-onto→ran 𝐹 ↔ (𝐹 ↾ 𝑥):𝑥–1-1-onto→ran 𝐹))
202	201	cbvrexvw 3217	. 2 ⊢ (∃𝑣 ∈ 𝒫 𝐴(𝐹 ↾ 𝑣):𝑣–1-1-onto→ran 𝐹 ↔ ∃𝑥 ∈ 𝒫 𝐴(𝐹 ↾ 𝑥):𝑥–1-1-onto→ran 𝐹)
203	197, 202	sylib 218	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝒫 𝐴(𝐹 ↾ 𝑥):𝑥–1-1-onto→ran 𝐹)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052  ∃wrex 3062  ∃!wreu 3341  Vcvv 3430   ⊆ wss 3890  ∅c0 4274  𝒫 cpw 4542  {csn 4568   class class class wbr 5086   ↦ cmpt 5167   Or wor 5532   We wwe 5577  ^◡ccnv 5624  dom cdm 5625  ran crn 5626   ↾ cres 5627   “ cima 5628   Fn wfn 6488  ⟶wf 6489  –1-1→wf1 6490  –onto→wfo 6491  –1-1-onto→wf1o 6492  ‘cfv 6493  ℩crio 7317

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318

This theorem is referenced by:  wessf1orn  45637