dfac4

Description: Equivalence of two versions of the Axiom of Choice. The right-hand side is Axiom AC of BellMachover p. 488. The proof does not depend on AC. (Contributed by NM, 24-Mar-2004) (Revised by Mario Carneiro, 26-Jun-2015)

		Ref	Expression
	Assertion	dfac4	$⊢ CHOICE \leftrightarrow \forall x \exists f (f Fn x \land \forall z \in x (z \neq \emptyset \to f (z) \in z))$

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		fveq1	$⊢ f = y \to f (z) = y (z)$
3	2	eleq1d	$⊢ f = y \to (f (z) \in z \leftrightarrow y (z) \in z)$
4	3	imbi2d	$⊢ f = y \to ((z \neq \emptyset \to f (z) \in z) \leftrightarrow (z \neq \emptyset \to y (z) \in z))$
5	4	ralbidv	$⊢ f = y \to (\forall z \in x (z \neq \emptyset \to f (z) \in z) \leftrightarrow \forall z \in x (z \neq \emptyset \to y (z) \in z))$
6	5	cbvexvw	$⊢ \exists f \forall z \in x (z \neq \emptyset \to f (z) \in z) \leftrightarrow \exists y \forall z \in x (z \neq \emptyset \to y (z) \in z)$
7		fvex	$⊢ y (w) \in V$
8		eqid	$⊢ (w \in x ⟼ y (w)) = (w \in x ⟼ y (w))$
9	7 8	fnmpti	$⊢ (w \in x ⟼ y (w)) Fn x$
10		fveq2	$⊢ w = z \to y (w) = y (z)$
11		fvex	$⊢ y (z) \in V$
12	10 8 11	fvmpt	$⊢ z \in x \to (w \in x ⟼ y (w)) (z) = y (z)$
13	12	eleq1d	$⊢ z \in x \to ((w \in x ⟼ y (w)) (z) \in z \leftrightarrow y (z) \in z)$
14	13	imbi2d	$⊢ z \in x \to ((z \neq \emptyset \to (w \in x ⟼ y (w)) (z) \in z) \leftrightarrow (z \neq \emptyset \to y (z) \in z))$
15	14	ralbiia	$⊢ \forall z \in x (z \neq \emptyset \to (w \in x ⟼ y (w)) (z) \in z) \leftrightarrow \forall z \in x (z \neq \emptyset \to y (z) \in z)$
16	15	anbi2i	$⊢ ((w \in x ⟼ y (w)) Fn x \land \forall z \in x (z \neq \emptyset \to (w \in x ⟼ y (w)) (z) \in z)) \leftrightarrow ((w \in x ⟼ y (w)) Fn x \land \forall z \in x (z \neq \emptyset \to y (z) \in z))$
17	9 16	mpbiran	$⊢ ((w \in x ⟼ y (w)) Fn x \land \forall z \in x (z \neq \emptyset \to (w \in x ⟼ y (w)) (z) \in z)) \leftrightarrow \forall z \in x (z \neq \emptyset \to y (z) \in z)$
18		fvrn0	$⊢ y (w) \in (ran y \cup \{\emptyset\})$
19	18	rgenw	$⊢ \forall w \in x y (w) \in (ran y \cup \{\emptyset\})$
20	8	fmpt	$⊢ \forall w \in x y (w) \in (ran y \cup \{\emptyset\}) \leftrightarrow (w \in x ⟼ y (w)) : x ⟶ ran y \cup \{\emptyset\}$
21	19 20	mpbi	$⊢ (w \in x ⟼ y (w)) : x ⟶ ran y \cup \{\emptyset\}$
22		vex	$⊢ x \in V$
23		vex	$⊢ y \in V$
24	23	rnex	$⊢ ran y \in V$
25		p0ex	$⊢ \{\emptyset\} \in V$
26	24 25	unex	$⊢ ran y \cup \{\emptyset\} \in V$
27		fex2	$⊢ ((w \in x ⟼ y (w)) : x ⟶ ran y \cup \{\emptyset\} \land x \in V \land ran y \cup \{\emptyset\} \in V) \to (w \in x ⟼ y (w)) \in V$
28	21 22 26 27	mp3an	$⊢ (w \in x ⟼ y (w)) \in V$
29		fneq1	$⊢ f = (w \in x ⟼ y (w)) \to (f Fn x \leftrightarrow (w \in x ⟼ y (w)) Fn x)$
30		fveq1	$⊢ f = (w \in x ⟼ y (w)) \to f (z) = (w \in x ⟼ y (w)) (z)$
31	30	eleq1d	$⊢ f = (w \in x ⟼ y (w)) \to (f (z) \in z \leftrightarrow (w \in x ⟼ y (w)) (z) \in z)$
32	31	imbi2d	$⊢ f = (w \in x ⟼ y (w)) \to ((z \neq \emptyset \to f (z) \in z) \leftrightarrow (z \neq \emptyset \to (w \in x ⟼ y (w)) (z) \in z))$
33	32	ralbidv	$⊢ f = (w \in x ⟼ y (w)) \to (\forall z \in x (z \neq \emptyset \to f (z) \in z) \leftrightarrow \forall z \in x (z \neq \emptyset \to (w \in x ⟼ y (w)) (z) \in z))$
34	29 33	anbi12d	$⊢ f = (w \in x ⟼ y (w)) \to ((f Fn x \land \forall z \in x (z \neq \emptyset \to f (z) \in z)) \leftrightarrow ((w \in x ⟼ y (w)) Fn x \land \forall z \in x (z \neq \emptyset \to (w \in x ⟼ y (w)) (z) \in z)))$
35	28 34	spcev	$⊢ ((w \in x ⟼ y (w)) Fn x \land \forall z \in x (z \neq \emptyset \to (w \in x ⟼ y (w)) (z) \in z)) \to \exists f (f Fn x \land \forall z \in x (z \neq \emptyset \to f (z) \in z))$
36	17 35	sylbir	$⊢ \forall z \in x (z \neq \emptyset \to y (z) \in z) \to \exists f (f Fn x \land \forall z \in x (z \neq \emptyset \to f (z) \in z))$
37	36	exlimiv	$⊢ \exists y \forall z \in x (z \neq \emptyset \to y (z) \in z) \to \exists f (f Fn x \land \forall z \in x (z \neq \emptyset \to f (z) \in z))$
38	6 37	sylbi	$⊢ \exists f \forall z \in x (z \neq \emptyset \to f (z) \in z) \to \exists f (f Fn x \land \forall z \in x (z \neq \emptyset \to f (z) \in z))$
39		exsimpr	$⊢ \exists f (f Fn x \land \forall z \in x (z \neq \emptyset \to f (z) \in z)) \to \exists f \forall z \in x (z \neq \emptyset \to f (z) \in z)$
40	38 39	impbii	$⊢ \exists f \forall z \in x (z \neq \emptyset \to f (z) \in z) \leftrightarrow \exists f (f Fn x \land \forall z \in x (z \neq \emptyset \to f (z) \in z))$
41	40	albii	$⊢ \forall x \exists f \forall z \in x (z \neq \emptyset \to f (z) \in z) \leftrightarrow \forall x \exists f (f Fn x \land \forall z \in x (z \neq \emptyset \to f (z) \in z))$
42	1 41	bitri	$⊢ CHOICE \leftrightarrow \forall x \exists f (f Fn x \land \forall z \in x (z \neq \emptyset \to f (z) \in z))$

Metamath Proof Explorer

Theorem dfac4

Proof