dfac2b

Description: Axiom of Choice (first form) of Enderton p. 49 implies our Axiom of Choice (in the form of ac3 ). The proof does not make use of AC. Note that the Axiom of Regularity is used by the proof. Specifically, elneq and preleq 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 .) (Contributed by NM, 5-Apr-2004) (Revised by Mario Carneiro, 26-Jun-2015) (Revised by AV, 16-Jun-2022)

		Ref	Expression
	Assertion	dfac2b	$⊢ CHOICE \to \forall x \exists y \forall z \in x (z \neq \emptyset \to \exists! w \in z \exists v \in y (z \in v \land w \in v))$

Proof

Step	Hyp	Ref	Expression
1		dfac3	$⊢ CHOICE \leftrightarrow \forall x \exists f \forall z \in x (z \neq \emptyset \to f (z) \in z)$
2		nfra1	$⊢ Ⅎ z \forall z \in x (z \neq \emptyset \to f (z) \in z)$
3		rsp	$⊢ \forall z \in x (z \neq \emptyset \to f (z) \in z) \to (z \in x \to (z \neq \emptyset \to f (z) \in z))$
4		equid	$⊢ z = z$
5		neeq1	$⊢ u = z \to (u \neq \emptyset \leftrightarrow z \neq \emptyset)$
6		eqeq1	$⊢ u = z \to (u = z \leftrightarrow z = z)$
7	5 6	anbi12d	$⊢ u = z \to ((u \neq \emptyset \land u = z) \leftrightarrow (z \neq \emptyset \land z = z))$
8	7	rspcev	$⊢ (z \in x \land (z \neq \emptyset \land z = z)) \to \exists u \in x (u \neq \emptyset \land u = z)$
9	4 8	mpanr2	$⊢ (z \in x \land z \neq \emptyset) \to \exists u \in x (u \neq \emptyset \land u = z)$
10		fveq2	$⊢ u = z \to f (u) = f (z)$
11	10	preq1d	$⊢ u = z \to \{f (u), u\} = \{f (z), u\}$
12		preq2	$⊢ u = z \to \{f (z), u\} = \{f (z), z\}$
13	11 12	eqtr2d	$⊢ u = z \to \{f (z), z\} = \{f (u), u\}$
14	13	anim2i	$⊢ (u \neq \emptyset \land u = z) \to (u \neq \emptyset \land \{f (z), z\} = \{f (u), u\})$
15	14	reximi	$⊢ \exists u \in x (u \neq \emptyset \land u = z) \to \exists u \in x (u \neq \emptyset \land \{f (z), z\} = \{f (u), u\})$
16	9 15	syl	$⊢ (z \in x \land z \neq \emptyset) \to \exists u \in x (u \neq \emptyset \land \{f (z), z\} = \{f (u), u\})$
17		prex	$⊢ \{f (z), z\} \in V$
18		eqeq1	$⊢ g = \{f (z), z\} \to (g = \{f (u), u\} \leftrightarrow \{f (z), z\} = \{f (u), u\})$
19	18	anbi2d	$⊢ g = \{f (z), z\} \to ((u \neq \emptyset \land g = \{f (u), u\}) \leftrightarrow (u \neq \emptyset \land \{f (z), z\} = \{f (u), u\}))$
20	19	rexbidv	$⊢ g = \{f (z), z\} \to (\exists u \in x (u \neq \emptyset \land g = \{f (u), u\}) \leftrightarrow \exists u \in x (u \neq \emptyset \land \{f (z), z\} = \{f (u), u\}))$
21	17 20	elab	$⊢ \{f (z), z\} \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} \leftrightarrow \exists u \in x (u \neq \emptyset \land \{f (z), z\} = \{f (u), u\})$
22	16 21	sylibr	$⊢ (z \in x \land z \neq \emptyset) \to \{f (z), z\} \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\}$
23		vex	$⊢ z \in V$
24	23	prid2	$⊢ z \in \{f (z), z\}$
25		fvex	$⊢ f (z) \in V$
26	25	prid1	$⊢ f (z) \in \{f (z), z\}$
27	24 26	pm3.2i	$⊢ (z \in \{f (z), z\} \land f (z) \in \{f (z), z\})$
28		eleq2	$⊢ v = \{f (z), z\} \to (z \in v \leftrightarrow z \in \{f (z), z\})$
29		eleq2	$⊢ v = \{f (z), z\} \to (f (z) \in v \leftrightarrow f (z) \in \{f (z), z\})$
30	28 29	anbi12d	$⊢ v = \{f (z), z\} \to ((z \in v \land f (z) \in v) \leftrightarrow (z \in \{f (z), z\} \land f (z) \in \{f (z), z\}))$
31	30	rspcev	$⊢ (\{f (z), z\} \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} \land (z \in \{f (z), z\} \land f (z) \in \{f (z), z\})) \to \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land f (z) \in v)$
32	22 27 31	sylancl	$⊢ (z \in x \land z \neq \emptyset) \to \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land f (z) \in v)$
33		eleq1	$⊢ w = f (z) \to (w \in z \leftrightarrow f (z) \in z)$
34		eleq1	$⊢ w = f (z) \to (w \in v \leftrightarrow f (z) \in v)$
35	34	anbi2d	$⊢ w = f (z) \to ((z \in v \land w \in v) \leftrightarrow (z \in v \land f (z) \in v))$
36	35	rexbidv	$⊢ w = f (z) \to (\exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v) \leftrightarrow \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land f (z) \in v))$
37	33 36	anbi12d	$⊢ w = f (z) \to ((w \in z \land \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v)) \leftrightarrow (f (z) \in z \land \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land f (z) \in v)))$
38	25 37	spcev	$⊢ (f (z) \in z \land \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land f (z) \in v)) \to \exists w (w \in z \land \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v))$
39	32 38	sylan2	$⊢ (f (z) \in z \land (z \in x \land z \neq \emptyset)) \to \exists w (w \in z \land \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v))$
40	39	ex	$⊢ f (z) \in z \to ((z \in x \land z \neq \emptyset) \to \exists w (w \in z \land \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v)))$
41	3 40	syl8	$⊢ \forall z \in x (z \neq \emptyset \to f (z) \in z) \to (z \in x \to (z \neq \emptyset \to ((z \in x \land z \neq \emptyset) \to \exists w (w \in z \land \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v)))))$
42	41	impd	$⊢ \forall z \in x (z \neq \emptyset \to f (z) \in z) \to ((z \in x \land z \neq \emptyset) \to ((z \in x \land z \neq \emptyset) \to \exists w (w \in z \land \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v))))$
43	42	pm2.43d	$⊢ \forall z \in x (z \neq \emptyset \to f (z) \in z) \to ((z \in x \land z \neq \emptyset) \to \exists w (w \in z \land \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v)))$
44		df-rex	$⊢ \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v) \leftrightarrow \exists v (v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} \land (z \in v \land w \in v))$
45		vex	$⊢ v \in V$
46		eqeq1	$⊢ g = v \to (g = \{f (u), u\} \leftrightarrow v = \{f (u), u\})$
47	46	anbi2d	$⊢ g = v \to ((u \neq \emptyset \land g = \{f (u), u\}) \leftrightarrow (u \neq \emptyset \land v = \{f (u), u\}))$
48	47	rexbidv	$⊢ g = v \to (\exists u \in x (u \neq \emptyset \land g = \{f (u), u\}) \leftrightarrow \exists u \in x (u \neq \emptyset \land v = \{f (u), u\}))$
49	45 48	elab	$⊢ v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} \leftrightarrow \exists u \in x (u \neq \emptyset \land v = \{f (u), u\})$
50		neeq1	$⊢ z = u \to (z \neq \emptyset \leftrightarrow u \neq \emptyset)$
51		fveq2	$⊢ z = u \to f (z) = f (u)$
52	51	eleq1d	$⊢ z = u \to (f (z) \in z \leftrightarrow f (u) \in z)$
53		eleq2	$⊢ z = u \to (f (u) \in z \leftrightarrow f (u) \in u)$
54	52 53	bitrd	$⊢ z = u \to (f (z) \in z \leftrightarrow f (u) \in u)$
55	50 54	imbi12d	$⊢ z = u \to ((z \neq \emptyset \to f (z) \in z) \leftrightarrow (u \neq \emptyset \to f (u) \in u))$
56	55	rspccv	$⊢ \forall z \in x (z \neq \emptyset \to f (z) \in z) \to (u \in x \to (u \neq \emptyset \to f (u) \in u))$
57		elneq	$⊢ w \in z \to w \neq z$
58	57	neneqd	$⊢ w \in z \to \neg w = z$
59		vex	$⊢ w \in V$
60		neqne	$⊢ \neg w = z \to w \neq z$
61		prel12g	$⊢ (w \in V \land z \in V \land w \neq z) \to (\{w, z\} = \{f (u), u\} \leftrightarrow (w \in \{f (u), u\} \land z \in \{f (u), u\}))$
62	59 23 60 61	mp3an12i	$⊢ \neg w = z \to (\{w, z\} = \{f (u), u\} \leftrightarrow (w \in \{f (u), u\} \land z \in \{f (u), u\}))$
63		eleq2	$⊢ v = \{f (u), u\} \to (w \in v \leftrightarrow w \in \{f (u), u\})$
64		eleq2	$⊢ v = \{f (u), u\} \to (z \in v \leftrightarrow z \in \{f (u), u\})$
65	63 64	anbi12d	$⊢ v = \{f (u), u\} \to ((w \in v \land z \in v) \leftrightarrow (w \in \{f (u), u\} \land z \in \{f (u), u\}))$
66		ancom	$⊢ (w \in v \land z \in v) \leftrightarrow (z \in v \land w \in v)$
67	65 66	bitr3di	$⊢ v = \{f (u), u\} \to ((w \in \{f (u), u\} \land z \in \{f (u), u\}) \leftrightarrow (z \in v \land w \in v))$
68	62 67	sylan9bbr	$⊢ (v = \{f (u), u\} \land \neg w = z) \to (\{w, z\} = \{f (u), u\} \leftrightarrow (z \in v \land w \in v))$
69	58 68	sylan2	$⊢ (v = \{f (u), u\} \land w \in z) \to (\{w, z\} = \{f (u), u\} \leftrightarrow (z \in v \land w \in v))$
70	69	adantrr	$⊢ (v = \{f (u), u\} \land (w \in z \land f (u) \in u)) \to (\{w, z\} = \{f (u), u\} \leftrightarrow (z \in v \land w \in v))$
71	70	pm5.32da	$⊢ v = \{f (u), u\} \to (((w \in z \land f (u) \in u) \land \{w, z\} = \{f (u), u\}) \leftrightarrow ((w \in z \land f (u) \in u) \land (z \in v \land w \in v)))$
72	23	preleq	$⊢ ((w \in z \land f (u) \in u) \land \{w, z\} = \{f (u), u\}) \to (w = f (u) \land z = u)$
73	71 72	syl6bir	$⊢ v = \{f (u), u\} \to (((w \in z \land f (u) \in u) \land (z \in v \land w \in v)) \to (w = f (u) \land z = u))$
74	51	eqeq2d	$⊢ z = u \to (w = f (z) \leftrightarrow w = f (u))$
75	74	biimparc	$⊢ (w = f (u) \land z = u) \to w = f (z)$
76	73 75	syl6	$⊢ v = \{f (u), u\} \to (((w \in z \land f (u) \in u) \land (z \in v \land w \in v)) \to w = f (z))$
77	76	exp4c	$⊢ v = \{f (u), u\} \to (w \in z \to (f (u) \in u \to ((z \in v \land w \in v) \to w = f (z))))$
78	77	com13	$⊢ f (u) \in u \to (w \in z \to (v = \{f (u), u\} \to ((z \in v \land w \in v) \to w = f (z))))$
79	56 78	syl8	$⊢ \forall z \in x (z \neq \emptyset \to f (z) \in z) \to (u \in x \to (u \neq \emptyset \to (w \in z \to (v = \{f (u), u\} \to ((z \in v \land w \in v) \to w = f (z))))))$
80	79	com4r	$⊢ w \in z \to (\forall z \in x (z \neq \emptyset \to f (z) \in z) \to (u \in x \to (u \neq \emptyset \to (v = \{f (u), u\} \to ((z \in v \land w \in v) \to w = f (z))))))$
81	80	imp	$⊢ (w \in z \land \forall z \in x (z \neq \emptyset \to f (z) \in z)) \to (u \in x \to (u \neq \emptyset \to (v = \{f (u), u\} \to ((z \in v \land w \in v) \to w = f (z)))))$
82	81	imp4a	$⊢ (w \in z \land \forall z \in x (z \neq \emptyset \to f (z) \in z)) \to (u \in x \to ((u \neq \emptyset \land v = \{f (u), u\}) \to ((z \in v \land w \in v) \to w = f (z))))$
83	82	com3l	$⊢ u \in x \to ((u \neq \emptyset \land v = \{f (u), u\}) \to ((w \in z \land \forall z \in x (z \neq \emptyset \to f (z) \in z)) \to ((z \in v \land w \in v) \to w = f (z))))$
84	83	rexlimiv	$⊢ \exists u \in x (u \neq \emptyset \land v = \{f (u), u\}) \to ((w \in z \land \forall z \in x (z \neq \emptyset \to f (z) \in z)) \to ((z \in v \land w \in v) \to w = f (z)))$
85	49 84	sylbi	$⊢ v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} \to ((w \in z \land \forall z \in x (z \neq \emptyset \to f (z) \in z)) \to ((z \in v \land w \in v) \to w = f (z)))$
86	85	expd	$⊢ v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} \to (w \in z \to (\forall z \in x (z \neq \emptyset \to f (z) \in z) \to ((z \in v \land w \in v) \to w = f (z))))$
87	86	com13	$⊢ \forall z \in x (z \neq \emptyset \to f (z) \in z) \to (w \in z \to (v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} \to ((z \in v \land w \in v) \to w = f (z))))$
88	87	imp4b	$⊢ (\forall z \in x (z \neq \emptyset \to f (z) \in z) \land w \in z) \to ((v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} \land (z \in v \land w \in v)) \to w = f (z))$
89	88	exlimdv	$⊢ (\forall z \in x (z \neq \emptyset \to f (z) \in z) \land w \in z) \to (\exists v (v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} \land (z \in v \land w \in v)) \to w = f (z))$
90	44 89	syl5bi	$⊢ (\forall z \in x (z \neq \emptyset \to f (z) \in z) \land w \in z) \to (\exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v) \to w = f (z))$
91	90	expimpd	$⊢ \forall z \in x (z \neq \emptyset \to f (z) \in z) \to ((w \in z \land \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v)) \to w = f (z))$
92	91	alrimiv	$⊢ \forall z \in x (z \neq \emptyset \to f (z) \in z) \to \forall w ((w \in z \land \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v)) \to w = f (z))$
93		mo2icl	$⊢ \forall w ((w \in z \land \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v)) \to w = f (z)) \to \exists^{*} w (w \in z \land \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v))$
94	92 93	syl	$⊢ \forall z \in x (z \neq \emptyset \to f (z) \in z) \to \exists^{*} w (w \in z \land \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v))$
95	43 94	jctird	$⊢ \forall z \in x (z \neq \emptyset \to f (z) \in z) \to ((z \in x \land z \neq \emptyset) \to (\exists w (w \in z \land \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v)) \land \exists^{*} w (w \in z \land \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v))))$
96		df-reu	$⊢ \exists! w \in z \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v) \leftrightarrow \exists! w (w \in z \land \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v))$
97		df-eu	$⊢ \exists! w (w \in z \land \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v)) \leftrightarrow (\exists w (w \in z \land \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v)) \land \exists^{*} w (w \in z \land \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v)))$
98	96 97	bitri	$⊢ \exists! w \in z \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v) \leftrightarrow (\exists w (w \in z \land \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v)) \land \exists^{*} w (w \in z \land \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v)))$
99	95 98	syl6ibr	$⊢ \forall z \in x (z \neq \emptyset \to f (z) \in z) \to ((z \in x \land z \neq \emptyset) \to \exists! w \in z \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v))$
100	99	expd	$⊢ \forall z \in x (z \neq \emptyset \to f (z) \in z) \to (z \in x \to (z \neq \emptyset \to \exists! w \in z \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v)))$
101	2 100	ralrimi	$⊢ \forall z \in x (z \neq \emptyset \to f (z) \in z) \to \forall z \in x (z \neq \emptyset \to \exists! w \in z \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v))$
102		vex	$⊢ f \in V$
103	102	rnex	$⊢ ran f \in V$
104		p0ex	$⊢ \{\emptyset\} \in V$
105	103 104	unex	$⊢ ran f \cup \{\emptyset\} \in V$
106		vex	$⊢ x \in V$
107	105 106	unex	$⊢ (ran f \cup \{\emptyset\}) \cup x \in V$
108	107	pwex	$⊢ 𝒫 ((ran f \cup \{\emptyset\}) \cup x) \in V$
109		ssun1	$⊢ ran f \cup \{\emptyset\} \subseteq (ran f \cup \{\emptyset\}) \cup x$
110		fvrn0	$⊢ f (u) \in (ran f \cup \{\emptyset\})$
111	109 110	sselii	$⊢ f (u) \in ((ran f \cup \{\emptyset\}) \cup x)$
112		elun2	$⊢ u \in x \to u \in ((ran f \cup \{\emptyset\}) \cup x)$
113		prssi	$⊢ (f (u) \in ((ran f \cup \{\emptyset\}) \cup x) \land u \in ((ran f \cup \{\emptyset\}) \cup x)) \to \{f (u), u\} \subseteq (ran f \cup \{\emptyset\}) \cup x$
114	111 112 113	sylancr	$⊢ u \in x \to \{f (u), u\} \subseteq (ran f \cup \{\emptyset\}) \cup x$
115		prex	$⊢ \{f (u), u\} \in V$
116	115	elpw	$⊢ \{f (u), u\} \in 𝒫 ((ran f \cup \{\emptyset\}) \cup x) \leftrightarrow \{f (u), u\} \subseteq (ran f \cup \{\emptyset\}) \cup x$
117	114 116	sylibr	$⊢ u \in x \to \{f (u), u\} \in 𝒫 ((ran f \cup \{\emptyset\}) \cup x)$
118		eleq1	$⊢ g = \{f (u), u\} \to (g \in 𝒫 ((ran f \cup \{\emptyset\}) \cup x) \leftrightarrow \{f (u), u\} \in 𝒫 ((ran f \cup \{\emptyset\}) \cup x))$
119	117 118	syl5ibrcom	$⊢ u \in x \to (g = \{f (u), u\} \to g \in 𝒫 ((ran f \cup \{\emptyset\}) \cup x))$
120	119	adantld	$⊢ u \in x \to ((u \neq \emptyset \land g = \{f (u), u\}) \to g \in 𝒫 ((ran f \cup \{\emptyset\}) \cup x))$
121	120	rexlimiv	$⊢ \exists u \in x (u \neq \emptyset \land g = \{f (u), u\}) \to g \in 𝒫 ((ran f \cup \{\emptyset\}) \cup x)$
122	121	abssi	$⊢ \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} \subseteq 𝒫 ((ran f \cup \{\emptyset\}) \cup x)$
123	108 122	ssexi	$⊢ \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} \in V$
124		rexeq	$⊢ y = \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} \to (\exists v \in y (z \in v \land w \in v) \leftrightarrow \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v))$
125	124	reubidv	$⊢ y = \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} \to (\exists! w \in z \exists v \in y (z \in v \land w \in v) \leftrightarrow \exists! w \in z \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v))$
126	125	imbi2d	$⊢ y = \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} \to ((z \neq \emptyset \to \exists! w \in z \exists v \in y (z \in v \land w \in v)) \leftrightarrow (z \neq \emptyset \to \exists! w \in z \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v)))$
127	126	ralbidv	$⊢ y = \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} \to (\forall z \in x (z \neq \emptyset \to \exists! w \in z \exists v \in y (z \in v \land w \in v)) \leftrightarrow \forall z \in x (z \neq \emptyset \to \exists! w \in z \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v)))$
128	123 127	spcev	$⊢ \forall z \in x (z \neq \emptyset \to \exists! w \in z \exists v \in \{g \| \exists u \in x (u \neq \emptyset \land g = \{f (u), u\})\} (z \in v \land w \in v)) \to \exists y \forall z \in x (z \neq \emptyset \to \exists! w \in z \exists v \in y (z \in v \land w \in v))$
129	101 128	syl	$⊢ \forall z \in x (z \neq \emptyset \to f (z) \in z) \to \exists y \forall z \in x (z \neq \emptyset \to \exists! w \in z \exists v \in y (z \in v \land w \in v))$
130	129	exlimiv	$⊢ \exists f \forall z \in x (z \neq \emptyset \to f (z) \in z) \to \exists y \forall z \in x (z \neq \emptyset \to \exists! w \in z \exists v \in y (z \in v \land w \in v))$
131	130	alimi	$⊢ \forall x \exists f \forall z \in x (z \neq \emptyset \to f (z) \in z) \to \forall x \exists y \forall z \in x (z \neq \emptyset \to \exists! w \in z \exists v \in y (z \in v \land w \in v))$
132	1 131	sylbi	$⊢ CHOICE \to \forall x \exists y \forall z \in x (z \neq \emptyset \to \exists! w \in z \exists v \in y (z \in v \land w \in v))$

Metamath Proof Explorer

Theorem dfac2b

Proof