Theorem wessf1ornlem 42722

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 5989	. . . . . . . 8 ⊢ (◡𝐹 “ {𝑢}) ⊆ dom 𝐹
3		wessf1ornlem.f	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 Fn 𝐴)
4	3	fndmd 6538	. . . . . . . . 9 ⊢ (𝜑 → dom 𝐹 = 𝐴)
5	4	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → dom 𝐹 = 𝐴)
6	2, 5	sseqtrid 3973	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (◡𝐹 “ {𝑢}) ⊆ 𝐴)
7		wessf1ornlem.r	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 We 𝐴)
8	7	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → 𝑅 We 𝐴)
9	2, 4	sseqtrid 3973	. . . . . . . . . . 11 ⊢ (𝜑 → (◡𝐹 “ {𝑢}) ⊆ 𝐴)
10	1, 9	ssexd 5248	. . . . . . . . . 10 ⊢ (𝜑 → (◡𝐹 “ {𝑢}) ∈ V)
11	10	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (◡𝐹 “ {𝑢}) ∈ V)
12		inisegn0 6006	. . . . . . . . . . 11 ⊢ (𝑢 ∈ ran 𝐹 ↔ (◡𝐹 “ {𝑢}) ≠ ∅)
13	12	biimpi 215	. . . . . . . . . 10 ⊢ (𝑢 ∈ ran 𝐹 → (◡𝐹 “ {𝑢}) ≠ ∅)
14	13	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (◡𝐹 “ {𝑢}) ≠ ∅)
15		wereu 5585	. . . . . . . . 9 ⊢ ((𝑅 We 𝐴 ∧ ((◡𝐹 “ {𝑢}) ∈ V ∧ (◡𝐹 “ {𝑢}) ⊆ 𝐴 ∧ (◡𝐹 “ {𝑢}) ≠ ∅)) → ∃!𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)
16	8, 11, 6, 14, 15	syl13anc 1371	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → ∃!𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)
17		riotacl 7250	. . . . . . . 8 ⊢ (∃!𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣 → (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ (◡𝐹 “ {𝑢}))
18	16, 17	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ (◡𝐹 “ {𝑢}))
19	6, 18	sseldd 3922	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ 𝐴)
20	19	ralrimiva 3103	. . . . 5 ⊢ (𝜑 → ∀𝑢 ∈ ran 𝐹(℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ 𝐴)
21		wessf1ornlem.g	. . . . . . 7 ⊢ 𝐺 = (𝑦 ∈ ran 𝐹 ↦ (℩𝑥 ∈ (◡𝐹 “ {𝑦})∀𝑧 ∈ (◡𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥))
22		sneq 4571	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑢 → {𝑦} = {𝑢})
23	22	imaeq2d 5969	. . . . . . . . . 10 ⊢ (𝑦 = 𝑢 → (◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑢}))
24	23	raleqdv 3348	. . . . . . . . . 10 ⊢ (𝑦 = 𝑢 → (∀𝑧 ∈ (◡𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥 ↔ ∀𝑧 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥))
25	23, 24	riotaeqbidv 7235	. . . . . . . . 9 ⊢ (𝑦 = 𝑢 → (℩𝑥 ∈ (◡𝐹 “ {𝑦})∀𝑧 ∈ (◡𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥) = (℩𝑥 ∈ (◡𝐹 “ {𝑢})∀𝑧 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥))
26		breq1 5077	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑡 → (𝑧𝑅𝑥 ↔ 𝑡𝑅𝑥))
27	26	notbid 318	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑡 → (¬ 𝑧𝑅𝑥 ↔ ¬ 𝑡𝑅𝑥))
28	27	cbvralvw 3383	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥 ↔ ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑥)
29		breq2 5078	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑣 → (𝑡𝑅𝑥 ↔ 𝑡𝑅𝑣))
30	29	notbid 318	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑣 → (¬ 𝑡𝑅𝑥 ↔ ¬ 𝑡𝑅𝑣))
31	30	ralbidv 3112	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑣 → (∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑥 ↔ ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
32	28, 31	syl5bb 283	. . . . . . . . . 10 ⊢ (𝑥 = 𝑣 → (∀𝑧 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥 ↔ ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
33	32	cbvriotavw 7242	. . . . . . . . 9 ⊢ (℩𝑥 ∈ (◡𝐹 “ {𝑢})∀𝑧 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥) = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)
34	25, 33	eqtrdi 2794	. . . . . . . 8 ⊢ (𝑦 = 𝑢 → (℩𝑥 ∈ (◡𝐹 “ {𝑦})∀𝑧 ∈ (◡𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥) = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
35	34	cbvmptv 5187	. . . . . . 7 ⊢ (𝑦 ∈ ran 𝐹 ↦ (℩𝑥 ∈ (◡𝐹 “ {𝑦})∀𝑧 ∈ (◡𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥)) = (𝑢 ∈ ran 𝐹 ↦ (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
36	21, 35	eqtri 2766	. . . . . 6 ⊢ 𝐺 = (𝑢 ∈ ran 𝐹 ↦ (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
37	36	rnmptss 6996	. . . . 5 ⊢ (∀𝑢 ∈ ran 𝐹(℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ 𝐴 → ran 𝐺 ⊆ 𝐴)
38	20, 37	syl 17	. . . 4 ⊢ (𝜑 → ran 𝐺 ⊆ 𝐴)
39	1, 38	sselpwd 5250	. . 3 ⊢ (𝜑 → ran 𝐺 ∈ 𝒫 𝐴)
40		dffn3 6613	. . . . . . 7 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹)
41	3, 40	sylib 217	. . . . . 6 ⊢ (𝜑 → 𝐹:𝐴⟶ran 𝐹)
42	41, 38	fssresd 6641	. . . . 5 ⊢ (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺⟶ran 𝐹)
43		fvres 6793	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ ran 𝐺 → ((𝐹 ↾ ran 𝐺)‘𝑤) = (𝐹‘𝑤))
44	43	eqcomd 2744	. . . . . . . . . . . 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 6793	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ ran 𝐺 → ((𝐹 ↾ ran 𝐺)‘𝑡) = (𝐹‘𝑡))
48	47	ad2antlr 724	. . . . . . . . . . 11 ⊢ (((𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → ((𝐹 ↾ ran 𝐺)‘𝑡) = (𝐹‘𝑡))
49	45, 46, 48	3eqtrd 2782	. . . . . . . . . 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 2744	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑤) = (𝐹‘𝑡) → (𝐹‘𝑡) = (𝐹‘𝑤))
56	55	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → (𝐹‘𝑡) = (𝐹‘𝑤))
57		eleq1w 2821	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑤 → (𝑏 ∈ ran 𝐺 ↔ 𝑤 ∈ ran 𝐺))
58	57	3anbi3d 1441	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑤 → ((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ↔ (𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑤 ∈ ran 𝐺)))
59		fveq2 6774	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑤 → (𝐹‘𝑏) = (𝐹‘𝑤))
60	59	eqeq2d 2749	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑤 → ((𝐹‘𝑡) = (𝐹‘𝑏) ↔ (𝐹‘𝑡) = (𝐹‘𝑤)))
61	58, 60	anbi12d 631	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑤 → (((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑏)) ↔ ((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑤 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑤))))
62		breq1 5077	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑤 → (𝑏𝑅𝑡 ↔ 𝑤𝑅𝑡))
63	62	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑤 → (¬ 𝑏𝑅𝑡 ↔ ¬ 𝑤𝑅𝑡))
64	61, 63	imbi12d 345	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑤 → ((((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑏)) → ¬ 𝑏𝑅𝑡) ↔ (((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑤 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑤)) → ¬ 𝑤𝑅𝑡)))
65		eleq1w 2821	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑡 → (𝑎 ∈ ran 𝐺 ↔ 𝑡 ∈ ran 𝐺))
66	65	3anbi2d 1440	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑡 → ((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ↔ (𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺)))
67		fveqeq2 6783	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑡 → ((𝐹‘𝑎) = (𝐹‘𝑏) ↔ (𝐹‘𝑡) = (𝐹‘𝑏)))
68	66, 67	anbi12d 631	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑡 → (((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ↔ ((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑏))))
69		breq2 5078	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑡 → (𝑏𝑅𝑎 ↔ 𝑏𝑅𝑡))
70	69	notbid 318	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑡 → (¬ 𝑏𝑅𝑎 ↔ ¬ 𝑏𝑅𝑡))
71	68, 70	imbi12d 345	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑡 → ((((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ¬ 𝑏𝑅𝑎) ↔ (((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑏)) → ¬ 𝑏𝑅𝑡)))
72		eleq1w 2821	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑏 → (𝑡 ∈ ran 𝐺 ↔ 𝑏 ∈ ran 𝐺))
73	72	3anbi3d 1441	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑏 → ((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ↔ (𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺)))
74		fveq2 6774	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑏 → (𝐹‘𝑡) = (𝐹‘𝑏))
75	74	eqeq2d 2749	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑏 → ((𝐹‘𝑎) = (𝐹‘𝑡) ↔ (𝐹‘𝑎) = (𝐹‘𝑏)))
76	73, 75	anbi12d 631	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑏 → (((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑡)) ↔ ((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑏))))
77		breq1 5077	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑏 → (𝑡𝑅𝑎 ↔ 𝑏𝑅𝑎))
78	77	notbid 318	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑏 → (¬ 𝑡𝑅𝑎 ↔ ¬ 𝑏𝑅𝑎))
79	76, 78	imbi12d 345	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑏 → ((((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑡)) → ¬ 𝑡𝑅𝑎) ↔ (((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ¬ 𝑏𝑅𝑎)))
80		eleq1w 2821	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑎 → (𝑤 ∈ ran 𝐺 ↔ 𝑎 ∈ ran 𝐺))
81	80	3anbi2d 1440	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑎 → ((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ↔ (𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺)))
82		fveqeq2 6783	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑎 → ((𝐹‘𝑤) = (𝐹‘𝑡) ↔ (𝐹‘𝑎) = (𝐹‘𝑡)))
83	81, 82	anbi12d 631	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑎 → (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ↔ ((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑡))))
84		breq2 5078	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑎 → (𝑡𝑅𝑤 ↔ 𝑡𝑅𝑎))
85	84	notbid 318	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑎 → (¬ 𝑡𝑅𝑤 ↔ ¬ 𝑡𝑅𝑎))
86	83, 85	imbi12d 345	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑎 → ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → ¬ 𝑡𝑅𝑤) ↔ (((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑡)) → ¬ 𝑡𝑅𝑎)))
87	36	elrnmpt 5865	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ V → (𝑤 ∈ ran 𝐺 ↔ ∃𝑢 ∈ ran 𝐹 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)))
88	87	elv 3438	. . . . . . . . . . . . . . . . . . 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 2744	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = 𝑤)
94		simp11 1202	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝜑)
95		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
96		breq2 5078	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑣 = 𝑤 → (𝑡𝑅𝑣 ↔ 𝑡𝑅𝑤))
97	96	notbid 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑣 = 𝑤 → (¬ 𝑡𝑅𝑣 ↔ ¬ 𝑡𝑅𝑤))
98	97	ralbidv 3112	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑣 = 𝑤 → (∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣 ↔ ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤))
99	98	cbvriotavw 7242	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = (℩𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
100	95, 99	eqtr2di 2795	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → (℩𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤)
101	100	3ad2ant3 1134	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (℩𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤)
102	98	cbvreuvw 3386	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∃!𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣 ↔ ∃!𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
103	16, 102	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → ∃!𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
104		riota1 7254	. . . . . . . . . . . . . . . . . . . . . . . . . 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 7258	. . . . . . . . . . . . . . . . . . . . 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 3921	. . . . . . . . . . . . . . . . . . . . . 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 6937	. . . . . . . . . . . . . . . . . . . . . . . 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 2778	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝐹‘𝑡) = 𝑢)
128		fniniseg 6937	. . . . . . . . . . . . . . . . . . . . . . 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 3132	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤 ∧ 𝑡 ∈ (◡𝐹 “ {𝑢})) → ¬ 𝑡𝑅𝑤)
135	115, 133, 134	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ¬ 𝑡𝑅𝑤)
136	135	rexlimdv3a 3215	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → (∃𝑢 ∈ ran 𝐹 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → ¬ 𝑡𝑅𝑤))
137	91, 136	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → ¬ 𝑡𝑅𝑤)
138	86, 137	chvarvv 2002	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑡)) → ¬ 𝑡𝑅𝑎)
139	79, 138	chvarvv 2002	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ¬ 𝑏𝑅𝑎)
140	71, 139	chvarvv 2002	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑏)) → ¬ 𝑏𝑅𝑡)
141	64, 140	chvarvv 2002	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑤 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑤)) → ¬ 𝑤𝑅𝑡)
142	51, 52, 53, 56, 141	syl31anc 1372	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → ¬ 𝑤𝑅𝑡)
143		weso 5580	. . . . . . . . . . . . . 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 3921	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐺) → 𝑤 ∈ 𝐴)
148	147	3adant3 1131	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) → 𝑤 ∈ 𝐴)
149	148	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → 𝑤 ∈ 𝐴)
150		sotrieq2 5533	. . . . . . . . . . 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 3123	. . . . 5 ⊢ (𝜑 → ∀𝑤 ∈ ran 𝐺∀𝑡 ∈ ran 𝐺(((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡))
157		dff13 7128	. . . . 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 7236	. . . . . . . . . . 11 ⊢ (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V
160	159	rgenw 3076	. . . . . . . . . 10 ⊢ ∀𝑢 ∈ ran 𝐹(℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V
161	36	fnmpt 6573	. . . . . . . . . 10 ⊢ (∀𝑢 ∈ ran 𝐹(℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V → 𝐺 Fn ran 𝐹)
162	160, 161	mp1i 13	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 Fn ran 𝐹)
163		dffn3 6613	. . . . . . . . 9 ⊢ (𝐺 Fn ran 𝐹 ↔ 𝐺:ran 𝐹⟶ran 𝐺)
164	162, 163	sylib 217	. . . . . . . 8 ⊢ (𝜑 → 𝐺:ran 𝐹⟶ran 𝐺)
165	164	ffvelrnda 6961	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (𝐺‘𝑢) ∈ ran 𝐺)
166	165	fvresd 6794	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → ((𝐹 ↾ ran 𝐺)‘(𝐺‘𝑢)) = (𝐹‘(𝐺‘𝑢)))
167		simpr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → 𝑢 ∈ ran 𝐹)
168	159	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V)
169	21, 34, 167, 168	fvmptd3 6898	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (𝐺‘𝑢) = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
170	169, 18	eqeltrd 2839	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (𝐺‘𝑢) ∈ (◡𝐹 “ {𝑢}))
171		fvex 6787	. . . . . . . . . . . 12 ⊢ (𝐺‘𝑢) ∈ V
172		eleq1 2826	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝐺‘𝑢) → (𝑤 ∈ (◡𝐹 “ {𝑢}) ↔ (𝐺‘𝑢) ∈ (◡𝐹 “ {𝑢})))
173		eleq1 2826	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝐺‘𝑢) → (𝑤 ∈ 𝐴 ↔ (𝐺‘𝑢) ∈ 𝐴))
174		fveqeq2 6783	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝐺‘𝑢) → ((𝐹‘𝑤) = 𝑢 ↔ (𝐹‘(𝐺‘𝑢)) = 𝑢))
175	173, 174	anbi12d 631	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝐺‘𝑢) → ((𝑤 ∈ 𝐴 ∧ (𝐹‘𝑤) = 𝑢) ↔ ((𝐺‘𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝑢)) = 𝑢)))
176	172, 175	bibi12d 346	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝐺‘𝑢) → ((𝑤 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑤 ∈ 𝐴 ∧ (𝐹‘𝑤) = 𝑢)) ↔ ((𝐺‘𝑢) ∈ (◡𝐹 “ {𝑢}) ↔ ((𝐺‘𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝑢)) = 𝑢))))
177	176	imbi2d 341	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝐺‘𝑢) → ((𝜑 → (𝑤 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑤 ∈ 𝐴 ∧ (𝐹‘𝑤) = 𝑢))) ↔ (𝜑 → ((𝐺‘𝑢) ∈ (◡𝐹 “ {𝑢}) ↔ ((𝐺‘𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝑢)) = 𝑢)))))
178	3, 122	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑤 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑤 ∈ 𝐴 ∧ (𝐹‘𝑤) = 𝑢)))
179	171, 177, 178	vtocl 3498	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐺‘𝑢) ∈ (◡𝐹 “ {𝑢}) ↔ ((𝐺‘𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝑢)) = 𝑢)))
180	179	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → ((𝐺‘𝑢) ∈ (◡𝐹 “ {𝑢}) ↔ ((𝐺‘𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝑢)) = 𝑢)))
181	170, 180	mpbid 231	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → ((𝐺‘𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝑢)) = 𝑢))
182	181	simprd 496	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (𝐹‘(𝐺‘𝑢)) = 𝑢)
183	166, 182	eqtr2d 2779	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → 𝑢 = ((𝐹 ↾ ran 𝐺)‘(𝐺‘𝑢)))
184		fveq2 6774	. . . . . . . 8 ⊢ (𝑤 = (𝐺‘𝑢) → ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘(𝐺‘𝑢)))
185	184	rspceeqv 3575	. . . . . . 7 ⊢ (((𝐺‘𝑢) ∈ ran 𝐺 ∧ 𝑢 = ((𝐹 ↾ ran 𝐺)‘(𝐺‘𝑢))) → ∃𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤))
186	165, 183, 185	syl2anc 584	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → ∃𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤))
187	186	ralrimiva 3103	. . . . 5 ⊢ (𝜑 → ∀𝑢 ∈ ran 𝐹∃𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤))
188		dffo3 6978	. . . . 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 6440	. . . 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 5886	. . . . 5 ⊢ (𝑣 = ran 𝐺 → (𝐹 ↾ 𝑣) = (𝐹 ↾ ran 𝐺))
193		id 22	. . . . 5 ⊢ (𝑣 = ran 𝐺 → 𝑣 = ran 𝐺)
194		eqidd 2739	. . . . 5 ⊢ (𝑣 = ran 𝐺 → ran 𝐹 = ran 𝐹)
195	192, 193, 194	f1oeq123d 6710	. . . 4 ⊢ (𝑣 = ran 𝐺 → ((𝐹 ↾ 𝑣):𝑣–1-1-onto→ran 𝐹 ↔ (𝐹 ↾ ran 𝐺):ran 𝐺–1-1-onto→ran 𝐹))
196	195	rspcev 3561	. . 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 5886	. . . 4 ⊢ (𝑣 = 𝑥 → (𝐹 ↾ 𝑣) = (𝐹 ↾ 𝑥))
199		id 22	. . . 4 ⊢ (𝑣 = 𝑥 → 𝑣 = 𝑥)
200		eqidd 2739	. . . 4 ⊢ (𝑣 = 𝑥 → ran 𝐹 = ran 𝐹)
201	198, 199, 200	f1oeq123d 6710	. . 3 ⊢ (𝑣 = 𝑥 → ((𝐹 ↾ 𝑣):𝑣–1-1-onto→ran 𝐹 ↔ (𝐹 ↾ 𝑥):𝑥–1-1-onto→ran 𝐹))
202	201	cbvrexvw 3384	. 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 1539   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  ∃wrex 3065  ∃!wreu 3066  Vcvv 3432   ⊆ wss 3887  ∅c0 4256  𝒫 cpw 4533  {csn 4561   class class class wbr 5074   ↦ cmpt 5157   Or wor 5502   We wwe 5543  ^◡ccnv 5588  dom cdm 5589  ran crn 5590   ↾ cres 5591   “ cima 5592   Fn wfn 6428  ⟶wf 6429  –1-1→wf1 6430  –onto→wfo 6431  –1-1-onto→wf1o 6432  ‘cfv 6433  ℩crio 7231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232

This theorem is referenced by:  wessf1orn  42723