Theorem dfac2b 10091

Description: Axiom of Choice (first form) of [Enderton] p. 49 implies our Axiom of Choice (in the form of ac3 10422). The proof does not make use of AC. Note that the Axiom of Regularity is used by the proof. Specifically, elneq 9558 and preleq 9576 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 10090.) (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 10081	. 2 ⊢ (CHOICE ↔ ∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))
2		nfra1 3262	. . . . . 6 ⊢ Ⅎ𝑧∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)
3		rsp 3226	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑧 ∈ 𝑥 → (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))
4		equid 2012	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑧 = 𝑧
5		neeq1 2988	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑧 → (𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅))
6		eqeq1 2734	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑧 → (𝑢 = 𝑧 ↔ 𝑧 = 𝑧))
7	5, 6	anbi12d 632	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑧 → ((𝑢 ≠ ∅ ∧ 𝑢 = 𝑧) ↔ (𝑧 ≠ ∅ ∧ 𝑧 = 𝑧)))
8	7	rspcev 3591	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 ∈ 𝑥 ∧ (𝑧 ≠ ∅ ∧ 𝑧 = 𝑧)) → ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑢 = 𝑧))
9	4, 8	mpanr2 704	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑢 = 𝑧))
10		fveq2 6861	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑧 → (𝑓‘𝑢) = (𝑓‘𝑧))
11	10	preq1d 4706	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑧 → {(𝑓‘𝑢), 𝑢} = {(𝑓‘𝑧), 𝑢})
12		preq2 4701	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑧 → {(𝑓‘𝑧), 𝑢} = {(𝑓‘𝑧), 𝑧})
13	11, 12	eqtr2d 2766	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑧 → {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢})
14	13	anim2i 617	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ≠ ∅ ∧ 𝑢 = 𝑧) → (𝑢 ≠ ∅ ∧ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢}))
15	14	reximi 3068	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑢 = 𝑧) → ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢}))
16	9, 15	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢}))
17		prex 5395	. . . . . . . . . . . . . . . . 17 ⊢ {(𝑓‘𝑧), 𝑧} ∈ V
18		eqeq1 2734	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = {(𝑓‘𝑧), 𝑧} → (𝑔 = {(𝑓‘𝑢), 𝑢} ↔ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢}))
19	18	anbi2d 630	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = {(𝑓‘𝑧), 𝑧} → ((𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢}) ↔ (𝑢 ≠ ∅ ∧ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢})))
20	19	rexbidv 3158	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = {(𝑓‘𝑧), 𝑧} → (∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢}) ↔ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢})))
21	17, 20	elab 3649	. . . . . . . . . . . . . . . 16 ⊢ ({(𝑓‘𝑧), 𝑧} ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ↔ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢}))
22	16, 21	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → {(𝑓‘𝑧), 𝑧} ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})})
23		vex 3454	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ V
24	23	prid2 4730	. . . . . . . . . . . . . . . 16 ⊢ 𝑧 ∈ {(𝑓‘𝑧), 𝑧}
25		fvex 6874	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓‘𝑧) ∈ V
26	25	prid1 4729	. . . . . . . . . . . . . . . 16 ⊢ (𝑓‘𝑧) ∈ {(𝑓‘𝑧), 𝑧}
27	24, 26	pm3.2i 470	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ {(𝑓‘𝑧), 𝑧} ∧ (𝑓‘𝑧) ∈ {(𝑓‘𝑧), 𝑧})
28		eleq2 2818	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = {(𝑓‘𝑧), 𝑧} → (𝑧 ∈ 𝑣 ↔ 𝑧 ∈ {(𝑓‘𝑧), 𝑧}))
29		eleq2 2818	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = {(𝑓‘𝑧), 𝑧} → ((𝑓‘𝑧) ∈ 𝑣 ↔ (𝑓‘𝑧) ∈ {(𝑓‘𝑧), 𝑧}))
30	28, 29	anbi12d 632	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = {(𝑓‘𝑧), 𝑧} → ((𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣) ↔ (𝑧 ∈ {(𝑓‘𝑧), 𝑧} ∧ (𝑓‘𝑧) ∈ {(𝑓‘𝑧), 𝑧})))
31	30	rspcev 3591	. . . . . . . . . . . . . . 15 ⊢ (({(𝑓‘𝑧), 𝑧} ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ∧ (𝑧 ∈ {(𝑓‘𝑧), 𝑧} ∧ (𝑓‘𝑧) ∈ {(𝑓‘𝑧), 𝑧})) → ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣))
32	22, 27, 31	sylancl 586	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣))
33		eleq1 2817	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = (𝑓‘𝑧) → (𝑤 ∈ 𝑧 ↔ (𝑓‘𝑧) ∈ 𝑧))
34		eleq1 2817	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = (𝑓‘𝑧) → (𝑤 ∈ 𝑣 ↔ (𝑓‘𝑧) ∈ 𝑣))
35	34	anbi2d 630	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = (𝑓‘𝑧) → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ (𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣)))
36	35	rexbidv 3158	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = (𝑓‘𝑧) → (∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣)))
37	33, 36	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝑓‘𝑧) → ((𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ↔ ((𝑓‘𝑧) ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣))))
38	25, 37	spcev 3575	. . . . . . . . . . . . . 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 3055	. . . . . . . . . . . . 13 ⊢ (∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ ∃𝑣(𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ∧ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
45		vex 3454	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑣 ∈ V
46		eqeq1 2734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑣 → (𝑔 = {(𝑓‘𝑢), 𝑢} ↔ 𝑣 = {(𝑓‘𝑢), 𝑢}))
47	46	anbi2d 630	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑣 → ((𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢}) ↔ (𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓‘𝑢), 𝑢})))
48	47	rexbidv 3158	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑣 → (∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢}) ↔ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓‘𝑢), 𝑢})))
49	45, 48	elab 3649	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ↔ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓‘𝑢), 𝑢}))
50		neeq1 2988	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 = 𝑢 → (𝑧 ≠ ∅ ↔ 𝑢 ≠ ∅))
51		fveq2 6861	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 = 𝑢 → (𝑓‘𝑧) = (𝑓‘𝑢))
52	51	eleq1d 2814	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 = 𝑢 → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘𝑢) ∈ 𝑧))
53		eleq2 2818	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 = 𝑢 → ((𝑓‘𝑢) ∈ 𝑧 ↔ (𝑓‘𝑢) ∈ 𝑢))
54	52, 53	bitrd 279	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 = 𝑢 → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘𝑢) ∈ 𝑢))
55	50, 54	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = 𝑢 → ((𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ (𝑢 ≠ ∅ → (𝑓‘𝑢) ∈ 𝑢)))
56	55	rspccv 3588	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑢 ∈ 𝑥 → (𝑢 ≠ ∅ → (𝑓‘𝑢) ∈ 𝑢)))
57		elneq 9558	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑤 ∈ 𝑧 → 𝑤 ≠ 𝑧)
58	57	neneqd 2931	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑤 ∈ 𝑧 → ¬ 𝑤 = 𝑧)
59		vex 3454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑤 ∈ V
60		neqne 2934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (¬ 𝑤 = 𝑧 → 𝑤 ≠ 𝑧)
61		prel12g 4831	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑤 ∈ V ∧ 𝑧 ∈ V ∧ 𝑤 ≠ 𝑧) → ({𝑤, 𝑧} = {(𝑓‘𝑢), 𝑢} ↔ (𝑤 ∈ {(𝑓‘𝑢), 𝑢} ∧ 𝑧 ∈ {(𝑓‘𝑢), 𝑢})))
62	59, 23, 60, 61	mp3an12i 1467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (¬ 𝑤 = 𝑧 → ({𝑤, 𝑧} = {(𝑓‘𝑢), 𝑢} ↔ (𝑤 ∈ {(𝑓‘𝑢), 𝑢} ∧ 𝑧 ∈ {(𝑓‘𝑢), 𝑢})))
63		eleq2 2818	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → (𝑤 ∈ 𝑣 ↔ 𝑤 ∈ {(𝑓‘𝑢), 𝑢}))
64		eleq2 2818	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9576	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑤 ∈ 𝑧 ∧ (𝑓‘𝑢) ∈ 𝑢) ∧ {𝑤, 𝑧} = {(𝑓‘𝑢), 𝑢}) → (𝑤 = (𝑓‘𝑢) ∧ 𝑧 = 𝑢))
73	71, 72	biimtrrdi 254	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → (((𝑤 ∈ 𝑧 ∧ (𝑓‘𝑢) ∈ 𝑢) ∧ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → (𝑤 = (𝑓‘𝑢) ∧ 𝑧 = 𝑢)))
74	51	eqeq2d 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3128	. . . . . . . . . . . . . . . . . 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 3688	. . . . . . . . . 10 ⊢ (∀𝑤((𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → 𝑤 = (𝑓‘𝑧)) → ∃*𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
94	92, 93	syl 17	. . . . . . . . 9 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∃*𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
95	43, 94	jctird 526	. . . . . . . 8 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → (∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ∧ ∃*𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))))
96		df-reu 3357	. . . . . . . . 9 ⊢ (∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ ∃!𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
97		df-eu 2563	. . . . . . . . 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 3454	. . . . . . . . . . 11 ⊢ 𝑓 ∈ V
103	102	rnex 7889	. . . . . . . . . 10 ⊢ ran 𝑓 ∈ V
104		p0ex 5342	. . . . . . . . . 10 ⊢ {∅} ∈ V
105	103, 104	unex 7723	. . . . . . . . 9 ⊢ (ran 𝑓 ∪ {∅}) ∈ V
106		vex 3454	. . . . . . . . 9 ⊢ 𝑥 ∈ V
107	105, 106	unex 7723	. . . . . . . 8 ⊢ ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ∈ V
108	107	pwex 5338	. . . . . . 7 ⊢ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ∈ V
109		ssun1 4144	. . . . . . . . . . . . . 14 ⊢ (ran 𝑓 ∪ {∅}) ⊆ ((ran 𝑓 ∪ {∅}) ∪ 𝑥)
110		fvrn0 6891	. . . . . . . . . . . . . 14 ⊢ (𝑓‘𝑢) ∈ (ran 𝑓 ∪ {∅})
111	109, 110	sselii 3946	. . . . . . . . . . . . 13 ⊢ (𝑓‘𝑢) ∈ ((ran 𝑓 ∪ {∅}) ∪ 𝑥)
112		elun2 4149	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝑥 → 𝑢 ∈ ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
113		prssi 4788	. . . . . . . . . . . . 13 ⊢ (((𝑓‘𝑢) ∈ ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ∧ 𝑢 ∈ ((ran 𝑓 ∪ {∅}) ∪ 𝑥)) → {(𝑓‘𝑢), 𝑢} ⊆ ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
114	111, 112, 113	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ 𝑥 → {(𝑓‘𝑢), 𝑢} ⊆ ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
115		prex 5395	. . . . . . . . . . . . 13 ⊢ {(𝑓‘𝑢), 𝑢} ∈ V
116	115	elpw 4570	. . . . . . . . . . . 12 ⊢ ({(𝑓‘𝑢), 𝑢} ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ↔ {(𝑓‘𝑢), 𝑢} ⊆ ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
117	114, 116	sylibr 234	. . . . . . . . . . 11 ⊢ (𝑢 ∈ 𝑥 → {(𝑓‘𝑢), 𝑢} ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
118		eleq1 2817	. . . . . . . . . . 11 ⊢ (𝑔 = {(𝑓‘𝑢), 𝑢} → (𝑔 ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ↔ {(𝑓‘𝑢), 𝑢} ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥)))
119	117, 118	syl5ibrcom 247	. . . . . . . . . 10 ⊢ (𝑢 ∈ 𝑥 → (𝑔 = {(𝑓‘𝑢), 𝑢} → 𝑔 ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥)))
120	119	adantld 490	. . . . . . . . 9 ⊢ (𝑢 ∈ 𝑥 → ((𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢}) → 𝑔 ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥)))
121	120	rexlimiv 3128	. . . . . . . 8 ⊢ (∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢}) → 𝑔 ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
122	121	abssi 4036	. . . . . . 7 ⊢ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ⊆ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥)
123	108, 122	ssexi 5280	. . . . . 6 ⊢ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ∈ V
124		rexeq 3297	. . . . . . . . 9 ⊢ (𝑦 = {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} → (∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
125	124	reubidv 3374	. . . . . . . 8 ⊢ (𝑦 = {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} → (∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
126	125	imbi2d 340	. . . . . . 7 ⊢ (𝑦 = {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} → ((𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ↔ (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))))
127	126	ralbidv 3157	. . . . . 6 ⊢ (𝑦 = {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} → (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ↔ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))))
128	123, 127	spcev 3575	. . . . 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 2109  ∃*wmo 2532  ∃!weu 2562  {cab 2708   ≠ wne 2926  ∀wral 3045  ∃wrex 3054  ∃!wreu 3354  Vcvv 3450   ∪ cun 3915   ⊆ wss 3917  ∅c0 4299  𝒫 cpw 4566  {csn 4592  {cpr 4594  ran crn 5642  ‘cfv 6514  CHOICEwac 10075

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-reg 9552

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-eprel 5541  df-fr 5594  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-fv 6522  df-ac 10076

This theorem is referenced by:  dfac2  10092