dfac2a

Description: Our Axiom of Choice (in the form of ac3 ) implies the Axiom of Choice (first form) of Enderton p. 49. The proof uses neither AC nor the Axiom of Regularity. See dfac2b for the converse (which does use the Axiom of Regularity). (Contributed by NM, 5-Apr-2004) (Revised by Mario Carneiro, 26-Jun-2015)

		Ref	Expression
	Assertion	dfac2a	$⊢ \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)) \to CHOICE$

Proof

Step	Hyp	Ref	Expression
1		riotauni	$⊢ \exists! w \in z \exists v \in y (z \in v \land w \in v) \to (ι w \in z \| \exists v \in y (z \in v \land w \in v)) = ⋃ \{w \in z \| \exists v \in y (z \in v \land w \in v)\}$
2		riotacl	$⊢ \exists! w \in z \exists v \in y (z \in v \land w \in v) \to (ι w \in z \| \exists v \in y (z \in v \land w \in v)) \in z$
3	1 2	eqeltrrd	$⊢ \exists! w \in z \exists v \in y (z \in v \land w \in v) \to ⋃ \{w \in z \| \exists v \in y (z \in v \land w \in v)\} \in z$
4		elequ2	$⊢ u = z \to (w \in u \leftrightarrow w \in z)$
5		elequ1	$⊢ u = z \to (u \in v \leftrightarrow z \in v)$
6	5	anbi1d	$⊢ u = z \to ((u \in v \land w \in v) \leftrightarrow (z \in v \land w \in v))$
7	6	rexbidv	$⊢ u = z \to (\exists v \in y (u \in v \land w \in v) \leftrightarrow \exists v \in y (z \in v \land w \in v))$
8	4 7	anbi12d	$⊢ u = z \to ((w \in u \land \exists v \in y (u \in v \land w \in v)) \leftrightarrow (w \in z \land \exists v \in y (z \in v \land w \in v)))$
9	8	rabbidva2	$⊢ u = z \to \{w \in u \| \exists v \in y (u \in v \land w \in v)\} = \{w \in z \| \exists v \in y (z \in v \land w \in v)\}$
10	9	unieqd	$⊢ u = z \to ⋃ \{w \in u \| \exists v \in y (u \in v \land w \in v)\} = ⋃ \{w \in z \| \exists v \in y (z \in v \land w \in v)\}$
11		eqid	$⊢ (u \in x ⟼ ⋃ \{w \in u \| \exists v \in y (u \in v \land w \in v)\}) = (u \in x ⟼ ⋃ \{w \in u \| \exists v \in y (u \in v \land w \in v)\})$
12		vex	$⊢ z \in V$
13	12	rabex	$⊢ \{w \in z \| \exists v \in y (z \in v \land w \in v)\} \in V$
14	13	uniex	$⊢ ⋃ \{w \in z \| \exists v \in y (z \in v \land w \in v)\} \in V$
15	10 11 14	fvmpt	$⊢ z \in x \to (u \in x ⟼ ⋃ \{w \in u \| \exists v \in y (u \in v \land w \in v)\}) (z) = ⋃ \{w \in z \| \exists v \in y (z \in v \land w \in v)\}$
16	15	eleq1d	$⊢ z \in x \to ((u \in x ⟼ ⋃ \{w \in u \| \exists v \in y (u \in v \land w \in v)\}) (z) \in z \leftrightarrow ⋃ \{w \in z \| \exists v \in y (z \in v \land w \in v)\} \in z)$
17	3 16	syl5ibr	$⊢ z \in x \to (\exists! w \in z \exists v \in y (z \in v \land w \in v) \to (u \in x ⟼ ⋃ \{w \in u \| \exists v \in y (u \in v \land w \in v)\}) (z) \in z)$
18	17	imim2d	$⊢ z \in x \to ((z \neq \emptyset \to \exists! w \in z \exists v \in y (z \in v \land w \in v)) \to (z \neq \emptyset \to (u \in x ⟼ ⋃ \{w \in u \| \exists v \in y (u \in v \land w \in v)\}) (z) \in z))$
19	18	ralimia	$⊢ \forall z \in x (z \neq \emptyset \to \exists! w \in z \exists v \in y (z \in v \land w \in v)) \to \forall z \in x (z \neq \emptyset \to (u \in x ⟼ ⋃ \{w \in u \| \exists v \in y (u \in v \land w \in v)\}) (z) \in z)$
20		ssrab2	$⊢ \{w \in u \| \exists v \in y (u \in v \land w \in v)\} \subseteq u$
21		elssuni	$⊢ u \in x \to u \subseteq ⋃ x$
22	20 21	sstrid	$⊢ u \in x \to \{w \in u \| \exists v \in y (u \in v \land w \in v)\} \subseteq ⋃ x$
23	22	unissd	$⊢ u \in x \to ⋃ \{w \in u \| \exists v \in y (u \in v \land w \in v)\} \subseteq ⋃ ⋃ x$
24		vex	$⊢ x \in V$
25	24	uniex	$⊢ ⋃ x \in V$
26	25	uniex	$⊢ ⋃ ⋃ x \in V$
27	26	elpw2	$⊢ ⋃ \{w \in u \| \exists v \in y (u \in v \land w \in v)\} \in 𝒫 ⋃ ⋃ x \leftrightarrow ⋃ \{w \in u \| \exists v \in y (u \in v \land w \in v)\} \subseteq ⋃ ⋃ x$
28	23 27	sylibr	$⊢ u \in x \to ⋃ \{w \in u \| \exists v \in y (u \in v \land w \in v)\} \in 𝒫 ⋃ ⋃ x$
29	11 28	fmpti	$⊢ (u \in x ⟼ ⋃ \{w \in u \| \exists v \in y (u \in v \land w \in v)\}) : x ⟶ 𝒫 ⋃ ⋃ x$
30	26	pwex	$⊢ 𝒫 ⋃ ⋃ x \in V$
31		fex2	$⊢ ((u \in x ⟼ ⋃ \{w \in u \| \exists v \in y (u \in v \land w \in v)\}) : x ⟶ 𝒫 ⋃ ⋃ x \land x \in V \land 𝒫 ⋃ ⋃ x \in V) \to (u \in x ⟼ ⋃ \{w \in u \| \exists v \in y (u \in v \land w \in v)\}) \in V$
32	29 24 30 31	mp3an	$⊢ (u \in x ⟼ ⋃ \{w \in u \| \exists v \in y (u \in v \land w \in v)\}) \in V$
33		fveq1	$⊢ f = (u \in x ⟼ ⋃ \{w \in u \| \exists v \in y (u \in v \land w \in v)\}) \to f (z) = (u \in x ⟼ ⋃ \{w \in u \| \exists v \in y (u \in v \land w \in v)\}) (z)$
34	33	eleq1d	$⊢ f = (u \in x ⟼ ⋃ \{w \in u \| \exists v \in y (u \in v \land w \in v)\}) \to (f (z) \in z \leftrightarrow (u \in x ⟼ ⋃ \{w \in u \| \exists v \in y (u \in v \land w \in v)\}) (z) \in z)$
35	34	imbi2d	$⊢ f = (u \in x ⟼ ⋃ \{w \in u \| \exists v \in y (u \in v \land w \in v)\}) \to ((z \neq \emptyset \to f (z) \in z) \leftrightarrow (z \neq \emptyset \to (u \in x ⟼ ⋃ \{w \in u \| \exists v \in y (u \in v \land w \in v)\}) (z) \in z))$
36	35	ralbidv	$⊢ f = (u \in x ⟼ ⋃ \{w \in u \| \exists v \in y (u \in v \land w \in v)\}) \to (\forall z \in x (z \neq \emptyset \to f (z) \in z) \leftrightarrow \forall z \in x (z \neq \emptyset \to (u \in x ⟼ ⋃ \{w \in u \| \exists v \in y (u \in v \land w \in v)\}) (z) \in z))$
37	32 36	spcev	$⊢ \forall z \in x (z \neq \emptyset \to (u \in x ⟼ ⋃ \{w \in u \| \exists v \in y (u \in v \land w \in v)\}) (z) \in z) \to \exists f \forall z \in x (z \neq \emptyset \to f (z) \in z)$
38	19 37	syl	$⊢ \forall z \in x (z \neq \emptyset \to \exists! w \in z \exists v \in y (z \in v \land w \in v)) \to \exists f \forall z \in x (z \neq \emptyset \to f (z) \in z)$
39	38	exlimiv	$⊢ \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)) \to \exists f \forall z \in x (z \neq \emptyset \to f (z) \in z)$
40	39	alimi	$⊢ \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)) \to \forall x \exists f \forall z \in x (z \neq \emptyset \to f (z) \in z)$
41		dfac3	$⊢ CHOICE \leftrightarrow \forall x \exists f \forall z \in x (z \neq \emptyset \to f (z) \in z)$
42	40 41	sylibr	$⊢ \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)) \to CHOICE$

Metamath Proof Explorer

Theorem dfac2a

Proof