Theorem dfac2b 10053

Description: Axiom of Choice (first form) of [Enderton] p. 49 implies our Axiom of Choice (in the form of ac3 10384). The proof does not make use of AC. Note that the Axiom of Regularity is used by the proof. Specifically, elneq 9517 and preleq 9537 that are referenced in the proof each make use of Regularity for their derivations. (The reverse implication can be derived without using Regularity; see dfac2a 10052.) (Contributed by NM, 5-Apr-2004.) (Revised by Mario Carneiro, 26-Jun-2015.) (Revised by AV, 16-Jun-2022.)

Assertion

Ref	Expression
dfac2b	⊢ (CHOICE → ∀𝑥∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))

Distinct variable group:   𝑥,𝑧,𝑦,𝑤,𝑣

Proof of Theorem dfac2b

Dummy variables 𝑓 𝑢 𝑔 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfac3 10043	. 2 ⊢ (CHOICE ↔ ∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))
2		nfra1 3262	. . . . . 6 ⊢ Ⅎ𝑧∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)
3		rsp 3226	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑧 ∈ 𝑥 → (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))
4		equid 2014	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑧 = 𝑧
5		neeq1 2995	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑧 → (𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅))
6		eqeq1 2741	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑧 → (𝑢 = 𝑧 ↔ 𝑧 = 𝑧))
7	5, 6	anbi12d 633	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑧 → ((𝑢 ≠ ∅ ∧ 𝑢 = 𝑧) ↔ (𝑧 ≠ ∅ ∧ 𝑧 = 𝑧)))
8	7	rspcev 3578	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 ∈ 𝑥 ∧ (𝑧 ≠ ∅ ∧ 𝑧 = 𝑧)) → ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑢 = 𝑧))
9	4, 8	mpanr2 705	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑢 = 𝑧))
10		fveq2 6842	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑧 → (𝑓‘𝑢) = (𝑓‘𝑧))
11	10	preq1d 4698	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑧 → {(𝑓‘𝑢), 𝑢} = {(𝑓‘𝑧), 𝑢})
12		preq2 4693	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑧 → {(𝑓‘𝑧), 𝑢} = {(𝑓‘𝑧), 𝑧})
13	11, 12	eqtr2d 2773	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑧 → {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢})
14	13	anim2i 618	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ≠ ∅ ∧ 𝑢 = 𝑧) → (𝑢 ≠ ∅ ∧ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢}))
15	14	reximi 3076	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑢 = 𝑧) → ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢}))
16	9, 15	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢}))
17		prex 5384	. . . . . . . . . . . . . . . . 17 ⊢ {(𝑓‘𝑧), 𝑧} ∈ V
18		eqeq1 2741	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = {(𝑓‘𝑧), 𝑧} → (𝑔 = {(𝑓‘𝑢), 𝑢} ↔ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢}))
19	18	anbi2d 631	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = {(𝑓‘𝑧), 𝑧} → ((𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢}) ↔ (𝑢 ≠ ∅ ∧ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢})))
20	19	rexbidv 3162	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = {(𝑓‘𝑧), 𝑧} → (∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢}) ↔ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢})))
21	17, 20	elab 3636	. . . . . . . . . . . . . . . 16 ⊢ ({(𝑓‘𝑧), 𝑧} ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ↔ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢}))
22	16, 21	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → {(𝑓‘𝑧), 𝑧} ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})})
23		vex 3446	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ V
24	23	prid2 4722	. . . . . . . . . . . . . . . 16 ⊢ 𝑧 ∈ {(𝑓‘𝑧), 𝑧}
25		fvex 6855	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓‘𝑧) ∈ V
26	25	prid1 4721	. . . . . . . . . . . . . . . 16 ⊢ (𝑓‘𝑧) ∈ {(𝑓‘𝑧), 𝑧}
27	24, 26	pm3.2i 470	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ {(𝑓‘𝑧), 𝑧} ∧ (𝑓‘𝑧) ∈ {(𝑓‘𝑧), 𝑧})
28		eleq2 2826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = {(𝑓‘𝑧), 𝑧} → (𝑧 ∈ 𝑣 ↔ 𝑧 ∈ {(𝑓‘𝑧), 𝑧}))
29		eleq2 2826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = {(𝑓‘𝑧), 𝑧} → ((𝑓‘𝑧) ∈ 𝑣 ↔ (𝑓‘𝑧) ∈ {(𝑓‘𝑧), 𝑧}))
30	28, 29	anbi12d 633	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = {(𝑓‘𝑧), 𝑧} → ((𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣) ↔ (𝑧 ∈ {(𝑓‘𝑧), 𝑧} ∧ (𝑓‘𝑧) ∈ {(𝑓‘𝑧), 𝑧})))
31	30	rspcev 3578	. . . . . . . . . . . . . . 15 ⊢ (({(𝑓‘𝑧), 𝑧} ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ∧ (𝑧 ∈ {(𝑓‘𝑧), 𝑧} ∧ (𝑓‘𝑧) ∈ {(𝑓‘𝑧), 𝑧})) → ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣))
32	22, 27, 31	sylancl 587	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣))
33		eleq1 2825	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = (𝑓‘𝑧) → (𝑤 ∈ 𝑧 ↔ (𝑓‘𝑧) ∈ 𝑧))
34		eleq1 2825	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = (𝑓‘𝑧) → (𝑤 ∈ 𝑣 ↔ (𝑓‘𝑧) ∈ 𝑣))
35	34	anbi2d 631	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = (𝑓‘𝑧) → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ (𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣)))
36	35	rexbidv 3162	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = (𝑓‘𝑧) → (∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣)))
37	33, 36	anbi12d 633	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝑓‘𝑧) → ((𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ↔ ((𝑓‘𝑧) ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣))))
38	25, 37	spcev 3562	. . . . . . . . . . . . . 14 ⊢ (((𝑓‘𝑧) ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣)) → ∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
39	32, 38	sylan2 594	. . . . . . . . . . . . 13 ⊢ (((𝑓‘𝑧) ∈ 𝑧 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅)) → ∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
40	39	ex 412	. . . . . . . . . . . 12 ⊢ ((𝑓‘𝑧) ∈ 𝑧 → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))))
41	3, 40	syl8 76	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑧 ∈ 𝑥 → (𝑧 ≠ ∅ → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))))))
42	41	impd 410	. . . . . . . . . 10 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))))
43	42	pm2.43d 53	. . . . . . . . 9 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))))
44		df-rex 3063	. . . . . . . . . . . . 13 ⊢ (∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ ∃𝑣(𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ∧ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
45		vex 3446	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑣 ∈ V
46		eqeq1 2741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑣 → (𝑔 = {(𝑓‘𝑢), 𝑢} ↔ 𝑣 = {(𝑓‘𝑢), 𝑢}))
47	46	anbi2d 631	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑣 → ((𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢}) ↔ (𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓‘𝑢), 𝑢})))
48	47	rexbidv 3162	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑣 → (∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢}) ↔ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓‘𝑢), 𝑢})))
49	45, 48	elab 3636	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ↔ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓‘𝑢), 𝑢}))
50		neeq1 2995	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 = 𝑢 → (𝑧 ≠ ∅ ↔ 𝑢 ≠ ∅))
51		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 = 𝑢 → (𝑓‘𝑧) = (𝑓‘𝑢))
52	51	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 = 𝑢 → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘𝑢) ∈ 𝑧))
53		eleq2 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 = 𝑢 → ((𝑓‘𝑢) ∈ 𝑧 ↔ (𝑓‘𝑢) ∈ 𝑢))
54	52, 53	bitrd 279	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 = 𝑢 → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘𝑢) ∈ 𝑢))
55	50, 54	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = 𝑢 → ((𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ (𝑢 ≠ ∅ → (𝑓‘𝑢) ∈ 𝑢)))
56	55	rspccv 3575	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑢 ∈ 𝑥 → (𝑢 ≠ ∅ → (𝑓‘𝑢) ∈ 𝑢)))
57		elneq 9517	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑤 ∈ 𝑧 → 𝑤 ≠ 𝑧)
58	57	neneqd 2938	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑤 ∈ 𝑧 → ¬ 𝑤 = 𝑧)
59		vex 3446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑤 ∈ V
60		neqne 2941	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (¬ 𝑤 = 𝑧 → 𝑤 ≠ 𝑧)
61		prel12g 4822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑤 ∈ V ∧ 𝑧 ∈ V ∧ 𝑤 ≠ 𝑧) → ({𝑤, 𝑧} = {(𝑓‘𝑢), 𝑢} ↔ (𝑤 ∈ {(𝑓‘𝑢), 𝑢} ∧ 𝑧 ∈ {(𝑓‘𝑢), 𝑢})))
62	59, 23, 60, 61	mp3an12i 1468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (¬ 𝑤 = 𝑧 → ({𝑤, 𝑧} = {(𝑓‘𝑢), 𝑢} ↔ (𝑤 ∈ {(𝑓‘𝑢), 𝑢} ∧ 𝑧 ∈ {(𝑓‘𝑢), 𝑢})))
63		eleq2 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → (𝑤 ∈ 𝑣 ↔ 𝑤 ∈ {(𝑓‘𝑢), 𝑢}))
64		eleq2 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → (𝑧 ∈ 𝑣 ↔ 𝑧 ∈ {(𝑓‘𝑢), 𝑢}))
65	63, 64	anbi12d 633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → ((𝑤 ∈ 𝑣 ∧ 𝑧 ∈ 𝑣) ↔ (𝑤 ∈ {(𝑓‘𝑢), 𝑢} ∧ 𝑧 ∈ {(𝑓‘𝑢), 𝑢})))
66		ancom 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑤 ∈ 𝑣 ∧ 𝑧 ∈ 𝑣) ↔ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))
67	65, 66	bitr3di 286	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → ((𝑤 ∈ {(𝑓‘𝑢), 𝑢} ∧ 𝑧 ∈ {(𝑓‘𝑢), 𝑢}) ↔ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
68	62, 67	sylan9bbr 510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑣 = {(𝑓‘𝑢), 𝑢} ∧ ¬ 𝑤 = 𝑧) → ({𝑤, 𝑧} = {(𝑓‘𝑢), 𝑢} ↔ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
69	58, 68	sylan2 594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑣 = {(𝑓‘𝑢), 𝑢} ∧ 𝑤 ∈ 𝑧) → ({𝑤, 𝑧} = {(𝑓‘𝑢), 𝑢} ↔ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
70	69	adantrr 718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑣 = {(𝑓‘𝑢), 𝑢} ∧ (𝑤 ∈ 𝑧 ∧ (𝑓‘𝑢) ∈ 𝑢)) → ({𝑤, 𝑧} = {(𝑓‘𝑢), 𝑢} ↔ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
71	70	pm5.32da 579	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → (((𝑤 ∈ 𝑧 ∧ (𝑓‘𝑢) ∈ 𝑢) ∧ {𝑤, 𝑧} = {(𝑓‘𝑢), 𝑢}) ↔ ((𝑤 ∈ 𝑧 ∧ (𝑓‘𝑢) ∈ 𝑢) ∧ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))))
72	23	preleq 9537	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑤 ∈ 𝑧 ∧ (𝑓‘𝑢) ∈ 𝑢) ∧ {𝑤, 𝑧} = {(𝑓‘𝑢), 𝑢}) → (𝑤 = (𝑓‘𝑢) ∧ 𝑧 = 𝑢))
73	71, 72	biimtrrdi 254	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → (((𝑤 ∈ 𝑧 ∧ (𝑓‘𝑢) ∈ 𝑢) ∧ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → (𝑤 = (𝑓‘𝑢) ∧ 𝑧 = 𝑢)))
74	51	eqeq2d 2748	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 = 𝑢 → (𝑤 = (𝑓‘𝑧) ↔ 𝑤 = (𝑓‘𝑢)))
75	74	biimparc 479	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑤 = (𝑓‘𝑢) ∧ 𝑧 = 𝑢) → 𝑤 = (𝑓‘𝑧))
76	73, 75	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → (((𝑤 ∈ 𝑧 ∧ (𝑓‘𝑢) ∈ 𝑢) ∧ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → 𝑤 = (𝑓‘𝑧)))
77	76	exp4c 432	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → (𝑤 ∈ 𝑧 → ((𝑓‘𝑢) ∈ 𝑢 → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧)))))
78	77	com13 88	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓‘𝑢) ∈ 𝑢 → (𝑤 ∈ 𝑧 → (𝑣 = {(𝑓‘𝑢), 𝑢} → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧)))))
79	56, 78	syl8 76	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑢 ∈ 𝑥 → (𝑢 ≠ ∅ → (𝑤 ∈ 𝑧 → (𝑣 = {(𝑓‘𝑢), 𝑢} → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧)))))))
80	79	com4r 94	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ 𝑧 → (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑢 ∈ 𝑥 → (𝑢 ≠ ∅ → (𝑣 = {(𝑓‘𝑢), 𝑢} → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧)))))))
81	80	imp 406	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑤 ∈ 𝑧 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → (𝑢 ∈ 𝑥 → (𝑢 ≠ ∅ → (𝑣 = {(𝑓‘𝑢), 𝑢} → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧))))))
82	81	imp4a 422	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤 ∈ 𝑧 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → (𝑢 ∈ 𝑥 → ((𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓‘𝑢), 𝑢}) → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧)))))
83	82	com3l 89	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ 𝑥 → ((𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓‘𝑢), 𝑢}) → ((𝑤 ∈ 𝑧 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧)))))
84	83	rexlimiv 3132	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓‘𝑢), 𝑢}) → ((𝑤 ∈ 𝑧 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧))))
85	49, 84	sylbi 217	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} → ((𝑤 ∈ 𝑧 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧))))
86	85	expd 415	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} → (𝑤 ∈ 𝑧 → (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧)))))
87	86	com13 88	. . . . . . . . . . . . . . 15 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑤 ∈ 𝑧 → (𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧)))))
88	87	imp4b 421	. . . . . . . . . . . . . 14 ⊢ ((∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ 𝑤 ∈ 𝑧) → ((𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ∧ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → 𝑤 = (𝑓‘𝑧)))
89	88	exlimdv 1935	. . . . . . . . . . . . 13 ⊢ ((∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ 𝑤 ∈ 𝑧) → (∃𝑣(𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ∧ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → 𝑤 = (𝑓‘𝑧)))
90	44, 89	biimtrid 242	. . . . . . . . . . . 12 ⊢ ((∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ 𝑤 ∈ 𝑧) → (∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧)))
91	90	expimpd 453	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ((𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → 𝑤 = (𝑓‘𝑧)))
92	91	alrimiv 1929	. . . . . . . . . 10 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∀𝑤((𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → 𝑤 = (𝑓‘𝑧)))
93		mo2icl 3674	. . . . . . . . . 10 ⊢ (∀𝑤((𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → 𝑤 = (𝑓‘𝑧)) → ∃*𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
94	92, 93	syl 17	. . . . . . . . 9 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∃*𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
95	43, 94	jctird 526	. . . . . . . 8 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → (∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ∧ ∃*𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))))
96		df-reu 3353	. . . . . . . . 9 ⊢ (∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ ∃!𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
97		df-eu 2570	. . . . . . . . 9 ⊢ (∃!𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ↔ (∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ∧ ∃*𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))))
98	96, 97	bitri 275	. . . . . . . 8 ⊢ (∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ (∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ∧ ∃*𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))))
99	95, 98	imbitrrdi 252	. . . . . . 7 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
100	99	expd 415	. . . . . 6 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑧 ∈ 𝑥 → (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))))
101	2, 100	ralrimi 3236	. . . . 5 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
102		vex 3446	. . . . . . . . . . 11 ⊢ 𝑓 ∈ V
103	102	rnex 7862	. . . . . . . . . 10 ⊢ ran 𝑓 ∈ V
104		p0ex 5331	. . . . . . . . . 10 ⊢ {∅} ∈ V
105	103, 104	unex 7699	. . . . . . . . 9 ⊢ (ran 𝑓 ∪ {∅}) ∈ V
106		vex 3446	. . . . . . . . 9 ⊢ 𝑥 ∈ V
107	105, 106	unex 7699	. . . . . . . 8 ⊢ ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ∈ V
108	107	pwex 5327	. . . . . . 7 ⊢ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ∈ V
109		ssun1 4132	. . . . . . . . . . . . . 14 ⊢ (ran 𝑓 ∪ {∅}) ⊆ ((ran 𝑓 ∪ {∅}) ∪ 𝑥)
110		fvrn0 6870	. . . . . . . . . . . . . 14 ⊢ (𝑓‘𝑢) ∈ (ran 𝑓 ∪ {∅})
111	109, 110	sselii 3932	. . . . . . . . . . . . 13 ⊢ (𝑓‘𝑢) ∈ ((ran 𝑓 ∪ {∅}) ∪ 𝑥)
112		elun2 4137	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝑥 → 𝑢 ∈ ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
113		prssi 4779	. . . . . . . . . . . . 13 ⊢ (((𝑓‘𝑢) ∈ ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ∧ 𝑢 ∈ ((ran 𝑓 ∪ {∅}) ∪ 𝑥)) → {(𝑓‘𝑢), 𝑢} ⊆ ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
114	111, 112, 113	sylancr 588	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ 𝑥 → {(𝑓‘𝑢), 𝑢} ⊆ ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
115		prex 5384	. . . . . . . . . . . . 13 ⊢ {(𝑓‘𝑢), 𝑢} ∈ V
116	115	elpw 4560	. . . . . . . . . . . 12 ⊢ ({(𝑓‘𝑢), 𝑢} ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ↔ {(𝑓‘𝑢), 𝑢} ⊆ ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
117	114, 116	sylibr 234	. . . . . . . . . . 11 ⊢ (𝑢 ∈ 𝑥 → {(𝑓‘𝑢), 𝑢} ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
118		eleq1 2825	. . . . . . . . . . 11 ⊢ (𝑔 = {(𝑓‘𝑢), 𝑢} → (𝑔 ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ↔ {(𝑓‘𝑢), 𝑢} ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥)))
119	117, 118	syl5ibrcom 247	. . . . . . . . . 10 ⊢ (𝑢 ∈ 𝑥 → (𝑔 = {(𝑓‘𝑢), 𝑢} → 𝑔 ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥)))
120	119	adantld 490	. . . . . . . . 9 ⊢ (𝑢 ∈ 𝑥 → ((𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢}) → 𝑔 ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥)))
121	120	rexlimiv 3132	. . . . . . . 8 ⊢ (∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢}) → 𝑔 ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
122	121	abssi 4022	. . . . . . 7 ⊢ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ⊆ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥)
123	108, 122	ssexi 5269	. . . . . 6 ⊢ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ∈ V
124		rexeq 3294	. . . . . . . . 9 ⊢ (𝑦 = {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} → (∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
125	124	reubidv 3368	. . . . . . . 8 ⊢ (𝑦 = {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} → (∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
126	125	imbi2d 340	. . . . . . 7 ⊢ (𝑦 = {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} → ((𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ↔ (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))))
127	126	ralbidv 3161	. . . . . 6 ⊢ (𝑦 = {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} → (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ↔ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))))
128	123, 127	spcev 3562	. . . . 5 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
129	101, 128	syl 17	. . . 4 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
130	129	exlimiv 1932	. . 3 ⊢ (∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
131	130	alimi 1813	. 2 ⊢ (∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∀𝑥∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
132	1, 131	sylbi 217	1 ⊢ (CHOICE → ∀𝑥∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∃*wmo 2538  ∃!weu 2569  {cab 2715   ≠ wne 2933  ∀wral 3052  ∃wrex 3062  ∃!wreu 3350  Vcvv 3442   ∪ cun 3901   ⊆ wss 3903  ∅c0 4287  𝒫 cpw 4556  {csn 4582  {cpr 4584  ran crn 5633  ‘cfv 6500  CHOICEwac 10037

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 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-reg 9509

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  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-reu 3353  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-eprel 5532  df-fr 5585  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-fv 6508  df-ac 10038

This theorem is referenced by:  dfac2  10054