dfac3

Description: Equivalence of two versions of the Axiom of Choice. The left-hand side is defined as the Axiom of Choice (first form) of Enderton p. 49. The right-hand side is the Axiom of Choice of TakeutiZaring p. 83. The proof does not depend on AC. (Contributed by NM, 24-Mar-2004) (Revised by Stefan O'Rear, 22-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		df-ac	$⊢ CHOICE \leftrightarrow \forall y \exists f (f \subseteq y \land f Fn dom y)$
2		vex	$⊢ x \in V$
3		vuniex	$⊢ ⋃ x \in V$
4	2 3	xpex	$⊢ x \times ⋃ x \in V$
5		simpl	$⊢ (w \in x \land v \in w) \to w \in x$
6		elunii	$⊢ (v \in w \land w \in x) \to v \in ⋃ x$
7	6	ancoms	$⊢ (w \in x \land v \in w) \to v \in ⋃ x$
8	5 7	jca	$⊢ (w \in x \land v \in w) \to (w \in x \land v \in ⋃ x)$
9	8	ssopab2i	$⊢ \{⟨w, v⟩ \| (w \in x \land v \in w)\} \subseteq \{⟨w, v⟩ \| (w \in x \land v \in ⋃ x)\}$
10		df-xp	$⊢ x \times ⋃ x = \{⟨w, v⟩ \| (w \in x \land v \in ⋃ x)\}$
11	9 10	sseqtrri	$⊢ \{⟨w, v⟩ \| (w \in x \land v \in w)\} \subseteq x \times ⋃ x$
12	4 11	ssexi	$⊢ \{⟨w, v⟩ \| (w \in x \land v \in w)\} \in V$
13		sseq2	$⊢ y = \{⟨w, v⟩ \| (w \in x \land v \in w)\} \to (f \subseteq y \leftrightarrow f \subseteq \{⟨w, v⟩ \| (w \in x \land v \in w)\})$
14		dmeq	$⊢ y = \{⟨w, v⟩ \| (w \in x \land v \in w)\} \to dom y = dom \{⟨w, v⟩ \| (w \in x \land v \in w)\}$
15	14	fneq2d	$⊢ y = \{⟨w, v⟩ \| (w \in x \land v \in w)\} \to (f Fn dom y \leftrightarrow f Fn dom \{⟨w, v⟩ \| (w \in x \land v \in w)\})$
16	13 15	anbi12d	$⊢ y = \{⟨w, v⟩ \| (w \in x \land v \in w)\} \to ((f \subseteq y \land f Fn dom y) \leftrightarrow (f \subseteq \{⟨w, v⟩ \| (w \in x \land v \in w)\} \land f Fn dom \{⟨w, v⟩ \| (w \in x \land v \in w)\}))$
17	16	exbidv	$⊢ y = \{⟨w, v⟩ \| (w \in x \land v \in w)\} \to (\exists f (f \subseteq y \land f Fn dom y) \leftrightarrow \exists f (f \subseteq \{⟨w, v⟩ \| (w \in x \land v \in w)\} \land f Fn dom \{⟨w, v⟩ \| (w \in x \land v \in w)\}))$
18	12 17	spcv	$⊢ \forall y \exists f (f \subseteq y \land f Fn dom y) \to \exists f (f \subseteq \{⟨w, v⟩ \| (w \in x \land v \in w)\} \land f Fn dom \{⟨w, v⟩ \| (w \in x \land v \in w)\})$
19		fndm	$⊢ f Fn dom \{⟨w, v⟩ \| (w \in x \land v \in w)\} \to dom f = dom \{⟨w, v⟩ \| (w \in x \land v \in w)\}$
20		dmopab	$⊢ dom \{⟨w, v⟩ \| (w \in x \land v \in w)\} = \{w \| \exists v (w \in x \land v \in w)\}$
21	20	eleq2i	$⊢ z \in dom \{⟨w, v⟩ \| (w \in x \land v \in w)\} \leftrightarrow z \in \{w \| \exists v (w \in x \land v \in w)\}$
22		vex	$⊢ z \in V$
23		elequ1	$⊢ w = z \to (w \in x \leftrightarrow z \in x)$
24		eleq2	$⊢ w = z \to (v \in w \leftrightarrow v \in z)$
25	23 24	anbi12d	$⊢ w = z \to ((w \in x \land v \in w) \leftrightarrow (z \in x \land v \in z))$
26	25	exbidv	$⊢ w = z \to (\exists v (w \in x \land v \in w) \leftrightarrow \exists v (z \in x \land v \in z))$
27	22 26	elab	$⊢ z \in \{w \| \exists v (w \in x \land v \in w)\} \leftrightarrow \exists v (z \in x \land v \in z)$
28		19.42v	$⊢ \exists v (z \in x \land v \in z) \leftrightarrow (z \in x \land \exists v v \in z)$
29		n0	$⊢ z \neq \emptyset \leftrightarrow \exists v v \in z$
30	29	anbi2i	$⊢ (z \in x \land z \neq \emptyset) \leftrightarrow (z \in x \land \exists v v \in z)$
31	28 30	bitr4i	$⊢ \exists v (z \in x \land v \in z) \leftrightarrow (z \in x \land z \neq \emptyset)$
32	21 27 31	3bitrri	$⊢ (z \in x \land z \neq \emptyset) \leftrightarrow z \in dom \{⟨w, v⟩ \| (w \in x \land v \in w)\}$
33		eleq2	$⊢ dom f = dom \{⟨w, v⟩ \| (w \in x \land v \in w)\} \to (z \in dom f \leftrightarrow z \in dom \{⟨w, v⟩ \| (w \in x \land v \in w)\})$
34	32 33	bitr4id	$⊢ dom f = dom \{⟨w, v⟩ \| (w \in x \land v \in w)\} \to ((z \in x \land z \neq \emptyset) \leftrightarrow z \in dom f)$
35	19 34	syl	$⊢ f Fn dom \{⟨w, v⟩ \| (w \in x \land v \in w)\} \to ((z \in x \land z \neq \emptyset) \leftrightarrow z \in dom f)$
36	35	adantl	$⊢ (f \subseteq \{⟨w, v⟩ \| (w \in x \land v \in w)\} \land f Fn dom \{⟨w, v⟩ \| (w \in x \land v \in w)\}) \to ((z \in x \land z \neq \emptyset) \leftrightarrow z \in dom f)$
37		fnfun	$⊢ f Fn dom \{⟨w, v⟩ \| (w \in x \land v \in w)\} \to Fun f$
38		funfvima3	$⊢ (Fun f \land f \subseteq \{⟨w, v⟩ \| (w \in x \land v \in w)\}) \to (z \in dom f \to f (z) \in \{⟨w, v⟩ \| (w \in x \land v \in w)\} [\{z\}])$
39	38	ancoms	$⊢ (f \subseteq \{⟨w, v⟩ \| (w \in x \land v \in w)\} \land Fun f) \to (z \in dom f \to f (z) \in \{⟨w, v⟩ \| (w \in x \land v \in w)\} [\{z\}])$
40	37 39	sylan2	$⊢ (f \subseteq \{⟨w, v⟩ \| (w \in x \land v \in w)\} \land f Fn dom \{⟨w, v⟩ \| (w \in x \land v \in w)\}) \to (z \in dom f \to f (z) \in \{⟨w, v⟩ \| (w \in x \land v \in w)\} [\{z\}])$
41	36 40	sylbid	$⊢ (f \subseteq \{⟨w, v⟩ \| (w \in x \land v \in w)\} \land f Fn dom \{⟨w, v⟩ \| (w \in x \land v \in w)\}) \to ((z \in x \land z \neq \emptyset) \to f (z) \in \{⟨w, v⟩ \| (w \in x \land v \in w)\} [\{z\}])$
42	41	imp	$⊢ ((f \subseteq \{⟨w, v⟩ \| (w \in x \land v \in w)\} \land f Fn dom \{⟨w, v⟩ \| (w \in x \land v \in w)\}) \land (z \in x \land z \neq \emptyset)) \to f (z) \in \{⟨w, v⟩ \| (w \in x \land v \in w)\} [\{z\}]$
43		imasng	$⊢ z \in V \to \{⟨w, v⟩ \| (w \in x \land v \in w)\} [\{z\}] = \{u \| z \{⟨w, v⟩ \| (w \in x \land v \in w)\} u\}$
44	43	elv	$⊢ \{⟨w, v⟩ \| (w \in x \land v \in w)\} [\{z\}] = \{u \| z \{⟨w, v⟩ \| (w \in x \land v \in w)\} u\}$
45		vex	$⊢ u \in V$
46		elequ1	$⊢ v = u \to (v \in z \leftrightarrow u \in z)$
47	46	anbi2d	$⊢ v = u \to ((z \in x \land v \in z) \leftrightarrow (z \in x \land u \in z))$
48		eqid	$⊢ \{⟨w, v⟩ \| (w \in x \land v \in w)\} = \{⟨w, v⟩ \| (w \in x \land v \in w)\}$
49	22 45 25 47 48	brab	$⊢ z \{⟨w, v⟩ \| (w \in x \land v \in w)\} u \leftrightarrow (z \in x \land u \in z)$
50	49	abbii	$⊢ \{u \| z \{⟨w, v⟩ \| (w \in x \land v \in w)\} u\} = \{u \| (z \in x \land u \in z)\}$
51	44 50	eqtri	$⊢ \{⟨w, v⟩ \| (w \in x \land v \in w)\} [\{z\}] = \{u \| (z \in x \land u \in z)\}$
52		ibar	$⊢ z \in x \to (u \in z \leftrightarrow (z \in x \land u \in z))$
53	52	abbi2dv	$⊢ z \in x \to z = \{u \| (z \in x \land u \in z)\}$
54	51 53	eqtr4id	$⊢ z \in x \to \{⟨w, v⟩ \| (w \in x \land v \in w)\} [\{z\}] = z$
55	54	eleq2d	$⊢ z \in x \to (f (z) \in \{⟨w, v⟩ \| (w \in x \land v \in w)\} [\{z\}] \leftrightarrow f (z) \in z)$
56	55	ad2antrl	$⊢ ((f \subseteq \{⟨w, v⟩ \| (w \in x \land v \in w)\} \land f Fn dom \{⟨w, v⟩ \| (w \in x \land v \in w)\}) \land (z \in x \land z \neq \emptyset)) \to (f (z) \in \{⟨w, v⟩ \| (w \in x \land v \in w)\} [\{z\}] \leftrightarrow f (z) \in z)$
57	42 56	mpbid	$⊢ ((f \subseteq \{⟨w, v⟩ \| (w \in x \land v \in w)\} \land f Fn dom \{⟨w, v⟩ \| (w \in x \land v \in w)\}) \land (z \in x \land z \neq \emptyset)) \to f (z) \in z$
58	57	exp32	$⊢ (f \subseteq \{⟨w, v⟩ \| (w \in x \land v \in w)\} \land f Fn dom \{⟨w, v⟩ \| (w \in x \land v \in w)\}) \to (z \in x \to (z \neq \emptyset \to f (z) \in z))$
59	58	ralrimiv	$⊢ (f \subseteq \{⟨w, v⟩ \| (w \in x \land v \in w)\} \land f Fn dom \{⟨w, v⟩ \| (w \in x \land v \in w)\}) \to \forall z \in x (z \neq \emptyset \to f (z) \in z)$
60	59	eximi	$⊢ \exists f (f \subseteq \{⟨w, v⟩ \| (w \in x \land v \in w)\} \land f Fn dom \{⟨w, v⟩ \| (w \in x \land v \in w)\}) \to \exists f \forall z \in x (z \neq \emptyset \to f (z) \in z)$
61	18 60	syl	$⊢ \forall y \exists f (f \subseteq y \land f Fn dom y) \to \exists f \forall z \in x (z \neq \emptyset \to f (z) \in z)$
62	61	alrimiv	$⊢ \forall y \exists f (f \subseteq y \land f Fn dom y) \to \forall x \exists f \forall z \in x (z \neq \emptyset \to f (z) \in z)$
63		eqid	$⊢ (w \in dom y ⟼ f (\{u \| w y u\})) = (w \in dom y ⟼ f (\{u \| w y u\}))$
64	63	aceq3lem	$⊢ \forall x \exists f \forall z \in x (z \neq \emptyset \to f (z) \in z) \to \exists f (f \subseteq y \land f Fn dom y)$
65	64	alrimiv	$⊢ \forall x \exists f \forall z \in x (z \neq \emptyset \to f (z) \in z) \to \forall y \exists f (f \subseteq y \land f Fn dom y)$
66	62 65	impbii	$⊢ \forall y \exists f (f \subseteq y \land f Fn dom y) \leftrightarrow \forall x \exists f \forall z \in x (z \neq \emptyset \to f (z) \in z)$
67	1 66	bitri	$⊢ CHOICE \leftrightarrow \forall x \exists f \forall z \in x (z \neq \emptyset \to f (z) \in z)$

Metamath Proof Explorer

Theorem dfac3

Proof