Theorem dfac2b 10171

Description: Axiom of Choice (first form) of [Enderton] p. 49 implies our Axiom of Choice (in the form of ac3 10502). The proof does not make use of AC. Note that the Axiom of Regularity is used by the proof. Specifically, elneq 9638 and preleq 9656 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 10170.) (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 10161	. 2 ⊢ (CHOICE ↔ ∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))
2		nfra1 3284	. . . . . 6 ⊢ Ⅎ𝑧∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)
3		rsp 3247	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑧 ∈ 𝑥 → (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))
4		equid 2011	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑧 = 𝑧
5		neeq1 3003	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑧 → (𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅))
6		eqeq1 2741	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑧 → (𝑢 = 𝑧 ↔ 𝑧 = 𝑧))
7	5, 6	anbi12d 632	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑧 → ((𝑢 ≠ ∅ ∧ 𝑢 = 𝑧) ↔ (𝑧 ≠ ∅ ∧ 𝑧 = 𝑧)))
8	7	rspcev 3622	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 ∈ 𝑥 ∧ (𝑧 ≠ ∅ ∧ 𝑧 = 𝑧)) → ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑢 = 𝑧))
9	4, 8	mpanr2 704	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑢 = 𝑧))
10		fveq2 6906	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑧 → (𝑓‘𝑢) = (𝑓‘𝑧))
11	10	preq1d 4739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑧 → {(𝑓‘𝑢), 𝑢} = {(𝑓‘𝑧), 𝑢})
12		preq2 4734	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑧 → {(𝑓‘𝑧), 𝑢} = {(𝑓‘𝑧), 𝑧})
13	11, 12	eqtr2d 2778	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑧 → {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢})
14	13	anim2i 617	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ≠ ∅ ∧ 𝑢 = 𝑧) → (𝑢 ≠ ∅ ∧ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢}))
15	14	reximi 3084	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑢 = 𝑧) → ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢}))
16	9, 15	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢}))
17		prex 5437	. . . . . . . . . . . . . . . . 17 ⊢ {(𝑓‘𝑧), 𝑧} ∈ V
18		eqeq1 2741	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = {(𝑓‘𝑧), 𝑧} → (𝑔 = {(𝑓‘𝑢), 𝑢} ↔ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢}))
19	18	anbi2d 630	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = {(𝑓‘𝑧), 𝑧} → ((𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢}) ↔ (𝑢 ≠ ∅ ∧ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢})))
20	19	rexbidv 3179	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = {(𝑓‘𝑧), 𝑧} → (∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢}) ↔ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢})))
21	17, 20	elab 3679	. . . . . . . . . . . . . . . 16 ⊢ ({(𝑓‘𝑧), 𝑧} ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ↔ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢}))
22	16, 21	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → {(𝑓‘𝑧), 𝑧} ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})})
23		vex 3484	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ V
24	23	prid2 4763	. . . . . . . . . . . . . . . 16 ⊢ 𝑧 ∈ {(𝑓‘𝑧), 𝑧}
25		fvex 6919	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓‘𝑧) ∈ V
26	25	prid1 4762	. . . . . . . . . . . . . . . 16 ⊢ (𝑓‘𝑧) ∈ {(𝑓‘𝑧), 𝑧}
27	24, 26	pm3.2i 470	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ {(𝑓‘𝑧), 𝑧} ∧ (𝑓‘𝑧) ∈ {(𝑓‘𝑧), 𝑧})
28		eleq2 2830	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = {(𝑓‘𝑧), 𝑧} → (𝑧 ∈ 𝑣 ↔ 𝑧 ∈ {(𝑓‘𝑧), 𝑧}))
29		eleq2 2830	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = {(𝑓‘𝑧), 𝑧} → ((𝑓‘𝑧) ∈ 𝑣 ↔ (𝑓‘𝑧) ∈ {(𝑓‘𝑧), 𝑧}))
30	28, 29	anbi12d 632	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = {(𝑓‘𝑧), 𝑧} → ((𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣) ↔ (𝑧 ∈ {(𝑓‘𝑧), 𝑧} ∧ (𝑓‘𝑧) ∈ {(𝑓‘𝑧), 𝑧})))
31	30	rspcev 3622	. . . . . . . . . . . . . . 15 ⊢ (({(𝑓‘𝑧), 𝑧} ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ∧ (𝑧 ∈ {(𝑓‘𝑧), 𝑧} ∧ (𝑓‘𝑧) ∈ {(𝑓‘𝑧), 𝑧})) → ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣))
32	22, 27, 31	sylancl 586	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣))
33		eleq1 2829	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = (𝑓‘𝑧) → (𝑤 ∈ 𝑧 ↔ (𝑓‘𝑧) ∈ 𝑧))
34		eleq1 2829	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = (𝑓‘𝑧) → (𝑤 ∈ 𝑣 ↔ (𝑓‘𝑧) ∈ 𝑣))
35	34	anbi2d 630	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = (𝑓‘𝑧) → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ (𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣)))
36	35	rexbidv 3179	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = (𝑓‘𝑧) → (∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣)))
37	33, 36	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝑓‘𝑧) → ((𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ↔ ((𝑓‘𝑧) ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣))))
38	25, 37	spcev 3606	. . . . . . . . . . . . . 14 ⊢ (((𝑓‘𝑧) ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣)) → ∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
39	32, 38	sylan2 593	. . . . . . . . . . . . 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 3071	. . . . . . . . . . . . 13 ⊢ (∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ ∃𝑣(𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ∧ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
45		vex 3484	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑣 ∈ V
46		eqeq1 2741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑣 → (𝑔 = {(𝑓‘𝑢), 𝑢} ↔ 𝑣 = {(𝑓‘𝑢), 𝑢}))
47	46	anbi2d 630	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑣 → ((𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢}) ↔ (𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓‘𝑢), 𝑢})))
48	47	rexbidv 3179	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑣 → (∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢}) ↔ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓‘𝑢), 𝑢})))
49	45, 48	elab 3679	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ↔ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓‘𝑢), 𝑢}))
50		neeq1 3003	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 = 𝑢 → (𝑧 ≠ ∅ ↔ 𝑢 ≠ ∅))
51		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 = 𝑢 → (𝑓‘𝑧) = (𝑓‘𝑢))
52	51	eleq1d 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 = 𝑢 → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘𝑢) ∈ 𝑧))
53		eleq2 2830	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 = 𝑢 → ((𝑓‘𝑢) ∈ 𝑧 ↔ (𝑓‘𝑢) ∈ 𝑢))
54	52, 53	bitrd 279	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 = 𝑢 → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘𝑢) ∈ 𝑢))
55	50, 54	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = 𝑢 → ((𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ (𝑢 ≠ ∅ → (𝑓‘𝑢) ∈ 𝑢)))
56	55	rspccv 3619	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑢 ∈ 𝑥 → (𝑢 ≠ ∅ → (𝑓‘𝑢) ∈ 𝑢)))
57		elneq 9638	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑤 ∈ 𝑧 → 𝑤 ≠ 𝑧)
58	57	neneqd 2945	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑤 ∈ 𝑧 → ¬ 𝑤 = 𝑧)
59		vex 3484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑤 ∈ V
60		neqne 2948	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (¬ 𝑤 = 𝑧 → 𝑤 ≠ 𝑧)
61		prel12g 4864	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑤 ∈ V ∧ 𝑧 ∈ V ∧ 𝑤 ≠ 𝑧) → ({𝑤, 𝑧} = {(𝑓‘𝑢), 𝑢} ↔ (𝑤 ∈ {(𝑓‘𝑢), 𝑢} ∧ 𝑧 ∈ {(𝑓‘𝑢), 𝑢})))
62	59, 23, 60, 61	mp3an12i 1467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (¬ 𝑤 = 𝑧 → ({𝑤, 𝑧} = {(𝑓‘𝑢), 𝑢} ↔ (𝑤 ∈ {(𝑓‘𝑢), 𝑢} ∧ 𝑧 ∈ {(𝑓‘𝑢), 𝑢})))
63		eleq2 2830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → (𝑤 ∈ 𝑣 ↔ 𝑤 ∈ {(𝑓‘𝑢), 𝑢}))
64		eleq2 2830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → (𝑧 ∈ 𝑣 ↔ 𝑧 ∈ {(𝑓‘𝑢), 𝑢}))
65	63, 64	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → ((𝑤 ∈ 𝑣 ∧ 𝑧 ∈ 𝑣) ↔ (𝑤 ∈ {(𝑓‘𝑢), 𝑢} ∧ 𝑧 ∈ {(𝑓‘𝑢), 𝑢})))
66		ancom 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑤 ∈ 𝑣 ∧ 𝑧 ∈ 𝑣) ↔ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))
67	65, 66	bitr3di 286	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → ((𝑤 ∈ {(𝑓‘𝑢), 𝑢} ∧ 𝑧 ∈ {(𝑓‘𝑢), 𝑢}) ↔ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
68	62, 67	sylan9bbr 510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑣 = {(𝑓‘𝑢), 𝑢} ∧ ¬ 𝑤 = 𝑧) → ({𝑤, 𝑧} = {(𝑓‘𝑢), 𝑢} ↔ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
69	58, 68	sylan2 593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑣 = {(𝑓‘𝑢), 𝑢} ∧ 𝑤 ∈ 𝑧) → ({𝑤, 𝑧} = {(𝑓‘𝑢), 𝑢} ↔ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
70	69	adantrr 717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑣 = {(𝑓‘𝑢), 𝑢} ∧ (𝑤 ∈ 𝑧 ∧ (𝑓‘𝑢) ∈ 𝑢)) → ({𝑤, 𝑧} = {(𝑓‘𝑢), 𝑢} ↔ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
71	70	pm5.32da 579	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → (((𝑤 ∈ 𝑧 ∧ (𝑓‘𝑢) ∈ 𝑢) ∧ {𝑤, 𝑧} = {(𝑓‘𝑢), 𝑢}) ↔ ((𝑤 ∈ 𝑧 ∧ (𝑓‘𝑢) ∈ 𝑢) ∧ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))))
72	23	preleq 9656	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3148	. . . . . . . . . . . . . . . . . 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 1933	. . . . . . . . . . . . 13 ⊢ ((∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ 𝑤 ∈ 𝑧) → (∃𝑣(𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ∧ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → 𝑤 = (𝑓‘𝑧)))
90	44, 89	biimtrid 242	. . . . . . . . . . . 12 ⊢ ((∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ 𝑤 ∈ 𝑧) → (∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧)))
91	90	expimpd 453	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ((𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → 𝑤 = (𝑓‘𝑧)))
92	91	alrimiv 1927	. . . . . . . . . 10 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∀𝑤((𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → 𝑤 = (𝑓‘𝑧)))
93		mo2icl 3720	. . . . . . . . . 10 ⊢ (∀𝑤((𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → 𝑤 = (𝑓‘𝑧)) → ∃*𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
94	92, 93	syl 17	. . . . . . . . 9 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∃*𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
95	43, 94	jctird 526	. . . . . . . 8 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → (∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ∧ ∃*𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))))
96		df-reu 3381	. . . . . . . . 9 ⊢ (∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ ∃!𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
97		df-eu 2569	. . . . . . . . 9 ⊢ (∃!𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ↔ (∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ∧ ∃*𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))))
98	96, 97	bitri 275	. . . . . . . 8 ⊢ (∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ (∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ∧ ∃*𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))))
99	95, 98	imbitrrdi 252	. . . . . . 7 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
100	99	expd 415	. . . . . 6 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑧 ∈ 𝑥 → (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))))
101	2, 100	ralrimi 3257	. . . . 5 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
102		vex 3484	. . . . . . . . . . 11 ⊢ 𝑓 ∈ V
103	102	rnex 7932	. . . . . . . . . 10 ⊢ ran 𝑓 ∈ V
104		p0ex 5384	. . . . . . . . . 10 ⊢ {∅} ∈ V
105	103, 104	unex 7764	. . . . . . . . 9 ⊢ (ran 𝑓 ∪ {∅}) ∈ V
106		vex 3484	. . . . . . . . 9 ⊢ 𝑥 ∈ V
107	105, 106	unex 7764	. . . . . . . 8 ⊢ ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ∈ V
108	107	pwex 5380	. . . . . . 7 ⊢ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ∈ V
109		ssun1 4178	. . . . . . . . . . . . . 14 ⊢ (ran 𝑓 ∪ {∅}) ⊆ ((ran 𝑓 ∪ {∅}) ∪ 𝑥)
110		fvrn0 6936	. . . . . . . . . . . . . 14 ⊢ (𝑓‘𝑢) ∈ (ran 𝑓 ∪ {∅})
111	109, 110	sselii 3980	. . . . . . . . . . . . 13 ⊢ (𝑓‘𝑢) ∈ ((ran 𝑓 ∪ {∅}) ∪ 𝑥)
112		elun2 4183	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝑥 → 𝑢 ∈ ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
113		prssi 4821	. . . . . . . . . . . . 13 ⊢ (((𝑓‘𝑢) ∈ ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ∧ 𝑢 ∈ ((ran 𝑓 ∪ {∅}) ∪ 𝑥)) → {(𝑓‘𝑢), 𝑢} ⊆ ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
114	111, 112, 113	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ 𝑥 → {(𝑓‘𝑢), 𝑢} ⊆ ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
115		prex 5437	. . . . . . . . . . . . 13 ⊢ {(𝑓‘𝑢), 𝑢} ∈ V
116	115	elpw 4604	. . . . . . . . . . . 12 ⊢ ({(𝑓‘𝑢), 𝑢} ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ↔ {(𝑓‘𝑢), 𝑢} ⊆ ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
117	114, 116	sylibr 234	. . . . . . . . . . 11 ⊢ (𝑢 ∈ 𝑥 → {(𝑓‘𝑢), 𝑢} ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
118		eleq1 2829	. . . . . . . . . . 11 ⊢ (𝑔 = {(𝑓‘𝑢), 𝑢} → (𝑔 ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ↔ {(𝑓‘𝑢), 𝑢} ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥)))
119	117, 118	syl5ibrcom 247	. . . . . . . . . 10 ⊢ (𝑢 ∈ 𝑥 → (𝑔 = {(𝑓‘𝑢), 𝑢} → 𝑔 ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥)))
120	119	adantld 490	. . . . . . . . 9 ⊢ (𝑢 ∈ 𝑥 → ((𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢}) → 𝑔 ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥)))
121	120	rexlimiv 3148	. . . . . . . 8 ⊢ (∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢}) → 𝑔 ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
122	121	abssi 4070	. . . . . . 7 ⊢ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ⊆ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥)
123	108, 122	ssexi 5322	. . . . . 6 ⊢ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ∈ V
124		rexeq 3322	. . . . . . . . 9 ⊢ (𝑦 = {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} → (∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
125	124	reubidv 3398	. . . . . . . 8 ⊢ (𝑦 = {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} → (∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
126	125	imbi2d 340	. . . . . . 7 ⊢ (𝑦 = {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} → ((𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ↔ (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))))
127	126	ralbidv 3178	. . . . . 6 ⊢ (𝑦 = {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} → (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ↔ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))))
128	123, 127	spcev 3606	. . . . 5 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
129	101, 128	syl 17	. . . 4 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
130	129	exlimiv 1930	. . 3 ⊢ (∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
131	130	alimi 1811	. 2 ⊢ (∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∀𝑥∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
132	1, 131	sylbi 217	1 ⊢ (CHOICE → ∀𝑥∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2108  ∃*wmo 2538  ∃!weu 2568  {cab 2714   ≠ wne 2940  ∀wral 3061  ∃wrex 3070  ∃!wreu 3378  Vcvv 3480   ∪ cun 3949   ⊆ wss 3951  ∅c0 4333  𝒫 cpw 4600  {csn 4626  {cpr 4628  ran crn 5686  ‘cfv 6561  CHOICEwac 10155

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-reg 9632

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-eprel 5584  df-fr 5637  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-fv 6569  df-ac 10156

This theorem is referenced by:  dfac2  10172