Theorem dfac2b 10248

Description: Axiom of Choice (first form) of [Enderton] p. 49 implies our Axiom of Choice (in the form of ac3 10579). The proof does not make use of AC. Note that the Axiom of Regularity is used by the proof. Specifically, elneq 9632 and preleq 9654 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 10247.) (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 10239	. 2 ⊢ (CHOICE ↔ ∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))
2		nfra1 3290	. . . . . 6 ⊢ Ⅎ𝑧∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)
3		rsp 3254	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑧 ∈ 𝑥 → (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))
4		equid 2047	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑧 = 𝑧
5		neeq1 3021	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑧 → (𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅))
6		eqeq1 2767	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑧 → (𝑢 = 𝑧 ↔ 𝑧 = 𝑧))
7	5, 6	anbi12d 644	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑧 → ((𝑢 ≠ ∅ ∧ 𝑢 = 𝑧) ↔ (𝑧 ≠ ∅ ∧ 𝑧 = 𝑧)))
8	7	rspcev 3580	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 ∈ 𝑥 ∧ (𝑧 ≠ ∅ ∧ 𝑧 = 𝑧)) → ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑢 = 𝑧))
9	4, 8	mpanr2 717	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑢 = 𝑧))
10		fveq2 6916	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑧 → (𝑓‘𝑢) = (𝑓‘𝑧))
11	10	preq1d 4702	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑧 → {(𝑓‘𝑢), 𝑢} = {(𝑓‘𝑧), 𝑢})
12		preq2 4697	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑧 → {(𝑓‘𝑧), 𝑢} = {(𝑓‘𝑧), 𝑧})
13	11, 12	eqtr2d 2799	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑧 → {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢})
14	13	anim2i 629	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ≠ ∅ ∧ 𝑢 = 𝑧) → (𝑢 ≠ ∅ ∧ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢}))
15	14	reximi 3104	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑢 = 𝑧) → ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢}))
16	9, 15	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢}))
17		prex 5403	. . . . . . . . . . . . . . . . 17 ⊢ {(𝑓‘𝑧), 𝑧} ∈ V
18		eqeq1 2767	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = {(𝑓‘𝑧), 𝑧} → (𝑔 = {(𝑓‘𝑢), 𝑢} ↔ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢}))
19	18	anbi2d 642	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = {(𝑓‘𝑧), 𝑧} → ((𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢}) ↔ (𝑢 ≠ ∅ ∧ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢})))
20	19	rexbidv 3190	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = {(𝑓‘𝑧), 𝑧} → (∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢}) ↔ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢})))
21	17, 20	elab 3636	. . . . . . . . . . . . . . . 16 ⊢ ({(𝑓‘𝑧), 𝑧} ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ↔ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢}))
22	16, 21	sylibr 237	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → {(𝑓‘𝑧), 𝑧} ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})})
23		vex 3458	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ V
24	23	prid2 4726	. . . . . . . . . . . . . . . 16 ⊢ 𝑧 ∈ {(𝑓‘𝑧), 𝑧}
25		fvex 6929	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓‘𝑧) ∈ V
26	25	prid1 4725	. . . . . . . . . . . . . . . 16 ⊢ (𝑓‘𝑧) ∈ {(𝑓‘𝑧), 𝑧}
27	24, 26	pm3.2i 476	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ {(𝑓‘𝑧), 𝑧} ∧ (𝑓‘𝑧) ∈ {(𝑓‘𝑧), 𝑧})
28		eleq2 2853	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = {(𝑓‘𝑧), 𝑧} → (𝑧 ∈ 𝑣 ↔ 𝑧 ∈ {(𝑓‘𝑧), 𝑧}))
29		eleq2 2853	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = {(𝑓‘𝑧), 𝑧} → ((𝑓‘𝑧) ∈ 𝑣 ↔ (𝑓‘𝑧) ∈ {(𝑓‘𝑧), 𝑧}))
30	28, 29	anbi12d 644	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = {(𝑓‘𝑧), 𝑧} → ((𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣) ↔ (𝑧 ∈ {(𝑓‘𝑧), 𝑧} ∧ (𝑓‘𝑧) ∈ {(𝑓‘𝑧), 𝑧})))
31	30	rspcev 3580	. . . . . . . . . . . . . . 15 ⊢ (({(𝑓‘𝑧), 𝑧} ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ∧ (𝑧 ∈ {(𝑓‘𝑧), 𝑧} ∧ (𝑓‘𝑧) ∈ {(𝑓‘𝑧), 𝑧})) → ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣))
32	22, 27, 31	sylancl 598	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣))
33		eleq1 2852	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = (𝑓‘𝑧) → (𝑤 ∈ 𝑧 ↔ (𝑓‘𝑧) ∈ 𝑧))
34		eleq1 2852	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = (𝑓‘𝑧) → (𝑤 ∈ 𝑣 ↔ (𝑓‘𝑧) ∈ 𝑣))
35	34	anbi2d 642	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = (𝑓‘𝑧) → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ (𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣)))
36	35	rexbidv 3190	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = (𝑓‘𝑧) → (∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣)))
37	33, 36	anbi12d 644	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝑓‘𝑧) → ((𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ↔ ((𝑓‘𝑧) ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣))))
38	25, 37	spcev 3564	. . . . . . . . . . . . . 14 ⊢ (((𝑓‘𝑧) ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣)) → ∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
39	32, 38	sylan2 605	. . . . . . . . . . . . 13 ⊢ (((𝑓‘𝑧) ∈ 𝑧 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅)) → ∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
40	39	ex 418	. . . . . . . . . . . 12 ⊢ ((𝑓‘𝑧) ∈ 𝑧 → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))))
41	3, 40	syl8 77	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑧 ∈ 𝑥 → (𝑧 ≠ ∅ → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))))))
42	41	impd 416	. . . . . . . . . 10 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))))
43	42	pm2.43d 54	. . . . . . . . 9 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))))
44		df-rex 3091	. . . . . . . . . . . . 13 ⊢ (∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ ∃𝑣(𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ∧ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
45		vex 3458	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑣 ∈ V
46		eqeq1 2767	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑣 → (𝑔 = {(𝑓‘𝑢), 𝑢} ↔ 𝑣 = {(𝑓‘𝑢), 𝑢}))
47	46	anbi2d 642	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑣 → ((𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢}) ↔ (𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓‘𝑢), 𝑢})))
48	47	rexbidv 3190	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑣 → (∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢}) ↔ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓‘𝑢), 𝑢})))
49	45, 48	elab 3636	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ↔ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓‘𝑢), 𝑢}))
50		neeq1 3021	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 = 𝑢 → (𝑧 ≠ ∅ ↔ 𝑢 ≠ ∅))
51		fveq2 6916	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 = 𝑢 → (𝑓‘𝑧) = (𝑓‘𝑢))
52	51	eleq1d 2849	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 = 𝑢 → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘𝑢) ∈ 𝑧))
53		eleq2 2853	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 = 𝑢 → ((𝑓‘𝑢) ∈ 𝑧 ↔ (𝑓‘𝑢) ∈ 𝑢))
54	52, 53	bitrd 282	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 = 𝑢 → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘𝑢) ∈ 𝑢))
55	50, 54	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = 𝑢 → ((𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ (𝑢 ≠ ∅ → (𝑓‘𝑢) ∈ 𝑢)))
56	55	rspccv 3577	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑢 ∈ 𝑥 → (𝑢 ≠ ∅ → (𝑓‘𝑢) ∈ 𝑢)))
57		elneq 9632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑤 ∈ 𝑧 → 𝑤 ≠ 𝑧)
58	57	neneqd 2964	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑤 ∈ 𝑧 → ¬ 𝑤 = 𝑧)
59		vex 3458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑤 ∈ V
60		neqne 2967	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (¬ 𝑤 = 𝑧 → 𝑤 ≠ 𝑧)
61		prel12g 4824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑤 ∈ V ∧ 𝑧 ∈ V ∧ 𝑤 ≠ 𝑧) → ({𝑤, 𝑧} = {(𝑓‘𝑢), 𝑢} ↔ (𝑤 ∈ {(𝑓‘𝑢), 𝑢} ∧ 𝑧 ∈ {(𝑓‘𝑢), 𝑢})))
62	59, 23, 60, 61	mp3an12i 1495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (¬ 𝑤 = 𝑧 → ({𝑤, 𝑧} = {(𝑓‘𝑢), 𝑢} ↔ (𝑤 ∈ {(𝑓‘𝑢), 𝑢} ∧ 𝑧 ∈ {(𝑓‘𝑢), 𝑢})))
63		eleq2 2853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → (𝑤 ∈ 𝑣 ↔ 𝑤 ∈ {(𝑓‘𝑢), 𝑢}))
64		eleq2 2853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → (𝑧 ∈ 𝑣 ↔ 𝑧 ∈ {(𝑓‘𝑢), 𝑢}))
65	63, 64	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → ((𝑤 ∈ 𝑣 ∧ 𝑧 ∈ 𝑣) ↔ (𝑤 ∈ {(𝑓‘𝑢), 𝑢} ∧ 𝑧 ∈ {(𝑓‘𝑢), 𝑢})))
66		ancom 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑤 ∈ 𝑣 ∧ 𝑧 ∈ 𝑣) ↔ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))
67	65, 66	bitr3di 289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → ((𝑤 ∈ {(𝑓‘𝑢), 𝑢} ∧ 𝑧 ∈ {(𝑓‘𝑢), 𝑢}) ↔ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
68	62, 67	sylan9bbr 520	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑣 = {(𝑓‘𝑢), 𝑢} ∧ ¬ 𝑤 = 𝑧) → ({𝑤, 𝑧} = {(𝑓‘𝑢), 𝑢} ↔ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
69	58, 68	sylan2 605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑣 = {(𝑓‘𝑢), 𝑢} ∧ 𝑤 ∈ 𝑧) → ({𝑤, 𝑧} = {(𝑓‘𝑢), 𝑢} ↔ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
70	69	adantrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑣 = {(𝑓‘𝑢), 𝑢} ∧ (𝑤 ∈ 𝑧 ∧ (𝑓‘𝑢) ∈ 𝑢)) → ({𝑤, 𝑧} = {(𝑓‘𝑢), 𝑢} ↔ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
71	70	pm5.32da 590	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → (((𝑤 ∈ 𝑧 ∧ (𝑓‘𝑢) ∈ 𝑢) ∧ {𝑤, 𝑧} = {(𝑓‘𝑢), 𝑢}) ↔ ((𝑤 ∈ 𝑧 ∧ (𝑓‘𝑢) ∈ 𝑢) ∧ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))))
72	23	preleq 9654	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑤 ∈ 𝑧 ∧ (𝑓‘𝑢) ∈ 𝑢) ∧ {𝑤, 𝑧} = {(𝑓‘𝑢), 𝑢}) → (𝑤 = (𝑓‘𝑢) ∧ 𝑧 = 𝑢))
73	71, 72	biimtrrdi 257	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → (((𝑤 ∈ 𝑧 ∧ (𝑓‘𝑢) ∈ 𝑢) ∧ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → (𝑤 = (𝑓‘𝑢) ∧ 𝑧 = 𝑢)))
74	51	eqeq2d 2774	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 = 𝑢 → (𝑤 = (𝑓‘𝑧) ↔ 𝑤 = (𝑓‘𝑢)))
75	74	biimparc 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑤 = (𝑓‘𝑢) ∧ 𝑧 = 𝑢) → 𝑤 = (𝑓‘𝑧))
76	73, 75	syl6 36	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → (((𝑤 ∈ 𝑧 ∧ (𝑓‘𝑢) ∈ 𝑢) ∧ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → 𝑤 = (𝑓‘𝑧)))
77	76	exp4c 438	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → (𝑤 ∈ 𝑧 → ((𝑓‘𝑢) ∈ 𝑢 → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧)))))
78	77	com13 89	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓‘𝑢) ∈ 𝑢 → (𝑤 ∈ 𝑧 → (𝑣 = {(𝑓‘𝑢), 𝑢} → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧)))))
79	56, 78	syl8 77	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑢 ∈ 𝑥 → (𝑢 ≠ ∅ → (𝑤 ∈ 𝑧 → (𝑣 = {(𝑓‘𝑢), 𝑢} → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧)))))))
80	79	com4r 95	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ 𝑧 → (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑢 ∈ 𝑥 → (𝑢 ≠ ∅ → (𝑣 = {(𝑓‘𝑢), 𝑢} → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧)))))))
81	80	imp 412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑤 ∈ 𝑧 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → (𝑢 ∈ 𝑥 → (𝑢 ≠ ∅ → (𝑣 = {(𝑓‘𝑢), 𝑢} → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧))))))
82	81	imp4a 428	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤 ∈ 𝑧 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → (𝑢 ∈ 𝑥 → ((𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓‘𝑢), 𝑢}) → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧)))))
83	82	com3l 90	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ 𝑥 → ((𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓‘𝑢), 𝑢}) → ((𝑤 ∈ 𝑧 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧)))))
84	83	rexlimiv 3160	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓‘𝑢), 𝑢}) → ((𝑤 ∈ 𝑧 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧))))
85	49, 84	sylbi 220	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} → ((𝑤 ∈ 𝑧 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧))))
86	85	expd 421	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} → (𝑤 ∈ 𝑧 → (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧)))))
87	86	com13 89	. . . . . . . . . . . . . . 15 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑤 ∈ 𝑧 → (𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧)))))
88	87	imp4b 427	. . . . . . . . . . . . . 14 ⊢ ((∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ 𝑤 ∈ 𝑧) → ((𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ∧ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → 𝑤 = (𝑓‘𝑧)))
89	88	exlimdv 1968	. . . . . . . . . . . . 13 ⊢ ((∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ 𝑤 ∈ 𝑧) → (∃𝑣(𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ∧ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → 𝑤 = (𝑓‘𝑧)))
90	44, 89	biimtrid 245	. . . . . . . . . . . 12 ⊢ ((∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ 𝑤 ∈ 𝑧) → (∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧)))
91	90	expimpd 459	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ((𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → 𝑤 = (𝑓‘𝑧)))
92	91	alrimiv 1962	. . . . . . . . . 10 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∀𝑤((𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → 𝑤 = (𝑓‘𝑧)))
93		mo2icl 3675	. . . . . . . . . 10 ⊢ (∀𝑤((𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → 𝑤 = (𝑓‘𝑧)) → ∃*𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
94	92, 93	syl 18	. . . . . . . . 9 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∃*𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
95	43, 94	jctird 536	. . . . . . . 8 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → (∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ∧ ∃*𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))))
96		df-reu 3370	. . . . . . . . 9 ⊢ (∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ ∃!𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
97		df-eu 2597	. . . . . . . . 9 ⊢ (∃!𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ↔ (∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ∧ ∃*𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))))
98	96, 97	bitri 278	. . . . . . . 8 ⊢ (∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ (∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ∧ ∃*𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))))
99	95, 98	imbitrrdi 255	. . . . . . 7 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
100	99	expd 421	. . . . . 6 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑧 ∈ 𝑥 → (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))))
101	2, 100	ralrimi 3264	. . . . 5 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
102		vex 3458	. . . . . . . . . . 11 ⊢ 𝑓 ∈ V
103	102	rnex 7956	. . . . . . . . . 10 ⊢ ran 𝑓 ∈ V
104		p0ex 5353	. . . . . . . . . 10 ⊢ {∅} ∈ V
105	103, 104	unex 7793	. . . . . . . . 9 ⊢ (ran 𝑓 ∪ {∅}) ∈ V
106		vex 3458	. . . . . . . . 9 ⊢ 𝑥 ∈ V
107	105, 106	unex 7793	. . . . . . . 8 ⊢ ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ∈ V
108	107	pwex 5349	. . . . . . 7 ⊢ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ∈ V
109		ssun1 4179	. . . . . . . . . . . . . 14 ⊢ (ran 𝑓 ∪ {∅}) ⊆ ((ran 𝑓 ∪ {∅}) ∪ 𝑥)
110		fvrn0 6944	. . . . . . . . . . . . . 14 ⊢ (𝑓‘𝑢) ∈ (ran 𝑓 ∪ {∅})
111	109, 110	sselii 3910	. . . . . . . . . . . . 13 ⊢ (𝑓‘𝑢) ∈ ((ran 𝑓 ∪ {∅}) ∪ 𝑥)
112		elun2 4184	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝑥 → 𝑢 ∈ ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
113		prssi 4782	. . . . . . . . . . . . 13 ⊢ (((𝑓‘𝑢) ∈ ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ∧ 𝑢 ∈ ((ran 𝑓 ∪ {∅}) ∪ 𝑥)) → {(𝑓‘𝑢), 𝑢} ⊆ ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
114	111, 112, 113	sylancr 599	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ 𝑥 → {(𝑓‘𝑢), 𝑢} ⊆ ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
115		prex 5403	. . . . . . . . . . . . 13 ⊢ {(𝑓‘𝑢), 𝑢} ∈ V
116	115	elpw 4564	. . . . . . . . . . . 12 ⊢ ({(𝑓‘𝑢), 𝑢} ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ↔ {(𝑓‘𝑢), 𝑢} ⊆ ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
117	114, 116	sylibr 237	. . . . . . . . . . 11 ⊢ (𝑢 ∈ 𝑥 → {(𝑓‘𝑢), 𝑢} ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
118		eleq1 2852	. . . . . . . . . . 11 ⊢ (𝑔 = {(𝑓‘𝑢), 𝑢} → (𝑔 ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ↔ {(𝑓‘𝑢), 𝑢} ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥)))
119	117, 118	syl5ibrcom 250	. . . . . . . . . 10 ⊢ (𝑢 ∈ 𝑥 → (𝑔 = {(𝑓‘𝑢), 𝑢} → 𝑔 ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥)))
120	119	adantld 496	. . . . . . . . 9 ⊢ (𝑢 ∈ 𝑥 → ((𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢}) → 𝑔 ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥)))
121	120	rexlimiv 3160	. . . . . . . 8 ⊢ (∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢}) → 𝑔 ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
122	121	abssi 3996	. . . . . . 7 ⊢ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ⊆ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥)
123	108, 122	ssexi 5291	. . . . . 6 ⊢ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ∈ V
124		rexeq 3319	. . . . . . . . 9 ⊢ (𝑦 = {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} → (∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
125	124	reubidv 3385	. . . . . . . 8 ⊢ (𝑦 = {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} → (∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
126	125	imbi2d 343	. . . . . . 7 ⊢ (𝑦 = {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} → ((𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ↔ (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))))
127	126	ralbidv 3189	. . . . . 6 ⊢ (𝑦 = {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} → (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ↔ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))))
128	123, 127	spcev 3564	. . . . 5 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
129	101, 128	syl 18	. . . 4 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
130	129	exlimiv 1965	. . 3 ⊢ (∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
131	130	alimi 1844	. 2 ⊢ (∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∀𝑥∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
132	1, 131	sylbi 220	1 ⊢ (CHOICE → ∀𝑥∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2147  ∃*wmo 2565  ∃!weu 2596  {cab 2741   ≠ wne 2959  ∀wral 3080  ∃wrex 3090  ∃!wreu 3367  Vcvv 3454   ⊆ wss 3900   ∪ cun 4152  ∅c0 4281  𝒫 cpw 4560  {csn 4588  {cpr 4590  ran crn 5659  ‘cfv 6566  CHOICEwac 10233

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783  ax-reg 9623

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-eprel 5558  df-fr 5611  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-fv 6574  df-ac 10234

This theorem is used by:  dfac2  10249