dfacacn

Description: A choice equivalent: every set has choice sets of every length. (Contributed by Mario Carneiro, 31-Aug-2015)

		Ref	Expression
	Assertion	dfacacn	$⊢ CHOICE \leftrightarrow \forall x \underline{AC} x = V$

Proof

Step	Hyp	Ref	Expression
1		acacni	$⊢ (CHOICE \land x \in V) \to \underline{AC} x = V$
2	1	elvd	$⊢ CHOICE \to \underline{AC} x = V$
3	2	alrimiv	$⊢ CHOICE \to \forall x \underline{AC} x = V$
4		vex	$⊢ y \in V$
5	4	difexi	$⊢ y ∖ \{\emptyset\} \in V$
6		acneq	$⊢ x = y ∖ \{\emptyset\} \to \underline{AC} x = \underline{AC} (y ∖ \{\emptyset\})$
7	6	eqeq1d	$⊢ x = y ∖ \{\emptyset\} \to (\underline{AC} x = V \leftrightarrow \underline{AC} (y ∖ \{\emptyset\}) = V)$
8	5 7	spcv	$⊢ \forall x \underline{AC} x = V \to \underline{AC} (y ∖ \{\emptyset\}) = V$
9		vuniex	$⊢ ⋃ y \in V$
10		id	$⊢ \underline{AC} (y ∖ \{\emptyset\}) = V \to \underline{AC} (y ∖ \{\emptyset\}) = V$
11	9 10	eleqtrrid	$⊢ \underline{AC} (y ∖ \{\emptyset\}) = V \to ⋃ y \in \underline{AC} (y ∖ \{\emptyset\})$
12		eldifi	$⊢ z \in (y ∖ \{\emptyset\}) \to z \in y$
13		elssuni	$⊢ z \in y \to z \subseteq ⋃ y$
14	12 13	syl	$⊢ z \in (y ∖ \{\emptyset\}) \to z \subseteq ⋃ y$
15		eldifsni	$⊢ z \in (y ∖ \{\emptyset\}) \to z \neq \emptyset$
16	14 15	jca	$⊢ z \in (y ∖ \{\emptyset\}) \to (z \subseteq ⋃ y \land z \neq \emptyset)$
17	16	rgen	$⊢ \forall z \in (y ∖ \{\emptyset\}) (z \subseteq ⋃ y \land z \neq \emptyset)$
18		acni2	$⊢ (⋃ y \in \underline{AC} (y ∖ \{\emptyset\}) \land \forall z \in (y ∖ \{\emptyset\}) (z \subseteq ⋃ y \land z \neq \emptyset)) \to \exists g (g : y ∖ \{\emptyset\} ⟶ ⋃ y \land \forall z \in (y ∖ \{\emptyset\}) g (z) \in z)$
19	11 17 18	sylancl	$⊢ \underline{AC} (y ∖ \{\emptyset\}) = V \to \exists g (g : y ∖ \{\emptyset\} ⟶ ⋃ y \land \forall z \in (y ∖ \{\emptyset\}) g (z) \in z)$
20	4	mptex	$⊢ (x \in y ⟼ g (x)) \in V$
21		simpr	$⊢ (g : y ∖ \{\emptyset\} ⟶ ⋃ y \land \forall z \in (y ∖ \{\emptyset\}) g (z) \in z) \to \forall z \in (y ∖ \{\emptyset\}) g (z) \in z$
22		eldifsn	$⊢ z \in (y ∖ \{\emptyset\}) \leftrightarrow (z \in y \land z \neq \emptyset)$
23	22	imbi1i	$⊢ (z \in (y ∖ \{\emptyset\}) \to (x \in y ⟼ g (x)) (z) \in z) \leftrightarrow ((z \in y \land z \neq \emptyset) \to (x \in y ⟼ g (x)) (z) \in z)$
24		fveq2	$⊢ x = z \to g (x) = g (z)$
25		eqid	$⊢ (x \in y ⟼ g (x)) = (x \in y ⟼ g (x))$
26		fvex	$⊢ g (z) \in V$
27	24 25 26	fvmpt	$⊢ z \in y \to (x \in y ⟼ g (x)) (z) = g (z)$
28	12 27	syl	$⊢ z \in (y ∖ \{\emptyset\}) \to (x \in y ⟼ g (x)) (z) = g (z)$
29	28	eleq1d	$⊢ z \in (y ∖ \{\emptyset\}) \to ((x \in y ⟼ g (x)) (z) \in z \leftrightarrow g (z) \in z)$
30	29	pm5.74i	$⊢ (z \in (y ∖ \{\emptyset\}) \to (x \in y ⟼ g (x)) (z) \in z) \leftrightarrow (z \in (y ∖ \{\emptyset\}) \to g (z) \in z)$
31		impexp	$⊢ ((z \in y \land z \neq \emptyset) \to (x \in y ⟼ g (x)) (z) \in z) \leftrightarrow (z \in y \to (z \neq \emptyset \to (x \in y ⟼ g (x)) (z) \in z))$
32	23 30 31	3bitr3i	$⊢ (z \in (y ∖ \{\emptyset\}) \to g (z) \in z) \leftrightarrow (z \in y \to (z \neq \emptyset \to (x \in y ⟼ g (x)) (z) \in z))$
33	32	ralbii2	$⊢ \forall z \in (y ∖ \{\emptyset\}) g (z) \in z \leftrightarrow \forall z \in y (z \neq \emptyset \to (x \in y ⟼ g (x)) (z) \in z)$
34	21 33	sylib	$⊢ (g : y ∖ \{\emptyset\} ⟶ ⋃ y \land \forall z \in (y ∖ \{\emptyset\}) g (z) \in z) \to \forall z \in y (z \neq \emptyset \to (x \in y ⟼ g (x)) (z) \in z)$
35		fvrn0	$⊢ g (x) \in (ran g \cup \{\emptyset\})$
36	35	rgenw	$⊢ \forall x \in y g (x) \in (ran g \cup \{\emptyset\})$
37	25	fmpt	$⊢ \forall x \in y g (x) \in (ran g \cup \{\emptyset\}) \leftrightarrow (x \in y ⟼ g (x)) : y ⟶ ran g \cup \{\emptyset\}$
38	36 37	mpbi	$⊢ (x \in y ⟼ g (x)) : y ⟶ ran g \cup \{\emptyset\}$
39		ffn	$⊢ (x \in y ⟼ g (x)) : y ⟶ ran g \cup \{\emptyset\} \to (x \in y ⟼ g (x)) Fn y$
40	38 39	ax-mp	$⊢ (x \in y ⟼ g (x)) Fn y$
41	34 40	jctil	$⊢ (g : y ∖ \{\emptyset\} ⟶ ⋃ y \land \forall z \in (y ∖ \{\emptyset\}) g (z) \in z) \to ((x \in y ⟼ g (x)) Fn y \land \forall z \in y (z \neq \emptyset \to (x \in y ⟼ g (x)) (z) \in z))$
42		fneq1	$⊢ f = (x \in y ⟼ g (x)) \to (f Fn y \leftrightarrow (x \in y ⟼ g (x)) Fn y)$
43		fveq1	$⊢ f = (x \in y ⟼ g (x)) \to f (z) = (x \in y ⟼ g (x)) (z)$
44	43	eleq1d	$⊢ f = (x \in y ⟼ g (x)) \to (f (z) \in z \leftrightarrow (x \in y ⟼ g (x)) (z) \in z)$
45	44	imbi2d	$⊢ f = (x \in y ⟼ g (x)) \to ((z \neq \emptyset \to f (z) \in z) \leftrightarrow (z \neq \emptyset \to (x \in y ⟼ g (x)) (z) \in z))$
46	45	ralbidv	$⊢ f = (x \in y ⟼ g (x)) \to (\forall z \in y (z \neq \emptyset \to f (z) \in z) \leftrightarrow \forall z \in y (z \neq \emptyset \to (x \in y ⟼ g (x)) (z) \in z))$
47	42 46	anbi12d	$⊢ f = (x \in y ⟼ g (x)) \to ((f Fn y \land \forall z \in y (z \neq \emptyset \to f (z) \in z)) \leftrightarrow ((x \in y ⟼ g (x)) Fn y \land \forall z \in y (z \neq \emptyset \to (x \in y ⟼ g (x)) (z) \in z)))$
48	47	spcegv	$⊢ (x \in y ⟼ g (x)) \in V \to (((x \in y ⟼ g (x)) Fn y \land \forall z \in y (z \neq \emptyset \to (x \in y ⟼ g (x)) (z) \in z)) \to \exists f (f Fn y \land \forall z \in y (z \neq \emptyset \to f (z) \in z)))$
49	20 41 48	mpsyl	$⊢ (g : y ∖ \{\emptyset\} ⟶ ⋃ y \land \forall z \in (y ∖ \{\emptyset\}) g (z) \in z) \to \exists f (f Fn y \land \forall z \in y (z \neq \emptyset \to f (z) \in z))$
50	49	exlimiv	$⊢ \exists g (g : y ∖ \{\emptyset\} ⟶ ⋃ y \land \forall z \in (y ∖ \{\emptyset\}) g (z) \in z) \to \exists f (f Fn y \land \forall z \in y (z \neq \emptyset \to f (z) \in z))$
51	8 19 50	3syl	$⊢ \forall x \underline{AC} x = V \to \exists f (f Fn y \land \forall z \in y (z \neq \emptyset \to f (z) \in z))$
52	51	alrimiv	$⊢ \forall x \underline{AC} x = V \to \forall y \exists f (f Fn y \land \forall z \in y (z \neq \emptyset \to f (z) \in z))$
53		dfac4	$⊢ CHOICE \leftrightarrow \forall y \exists f (f Fn y \land \forall z \in y (z \neq \emptyset \to f (z) \in z))$
54	52 53	sylibr	$⊢ \forall x \underline{AC} x = V \to CHOICE$
55	3 54	impbii	$⊢ CHOICE \leftrightarrow \forall x \underline{AC} x = V$

Metamath Proof Explorer

Theorem dfacacn

Proof