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		eldifsn	$⊢ z \in (y ∖ \{\emptyset\}) \leftrightarrow (z \in y \land z \neq \emptyset)$
22	21	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)$
23		fveq2	$⊢ x = z \to g (x) = g (z)$
24		eqid	$⊢ (x \in y ⟼ g (x)) = (x \in y ⟼ g (x))$
25		fvex	$⊢ g (z) \in V$
26	23 24 25	fvmpt	$⊢ z \in y \to (x \in y ⟼ g (x)) (z) = g (z)$
27	12 26	syl	$⊢ z \in (y ∖ \{\emptyset\}) \to (x \in y ⟼ g (x)) (z) = g (z)$
28	27	eleq1d	$⊢ z \in (y ∖ \{\emptyset\}) \to ((x \in y ⟼ g (x)) (z) \in z \leftrightarrow g (z) \in z)$
29	28	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)$
30		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))$
31	22 29 30	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))$
32	31	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)$
33	32	bilani	$⊢ (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)$
34		fvrn0	$⊢ g (x) \in (ran g \cup \{\emptyset\})$
35	34	rgenw	$⊢ \forall x \in y g (x) \in (ran g \cup \{\emptyset\})$
36	24	fmpt	$⊢ \forall x \in y g (x) \in (ran g \cup \{\emptyset\}) \leftrightarrow (x \in y ⟼ g (x)) : y ⟶ ran g \cup \{\emptyset\}$
37	35 36	mpbi	$⊢ (x \in y ⟼ g (x)) : y ⟶ ran g \cup \{\emptyset\}$
38		ffn	$⊢ (x \in y ⟼ g (x)) : y ⟶ ran g \cup \{\emptyset\} \to (x \in y ⟼ g (x)) Fn y$
39	37 38	ax-mp	$⊢ (x \in y ⟼ g (x)) Fn y$
40	33 39	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))$
41		fneq1	$⊢ f = (x \in y ⟼ g (x)) \to (f Fn y \leftrightarrow (x \in y ⟼ g (x)) Fn y)$
42		fveq1	$⊢ f = (x \in y ⟼ g (x)) \to f (z) = (x \in y ⟼ g (x)) (z)$
43	42	eleq1d	$⊢ f = (x \in y ⟼ g (x)) \to (f (z) \in z \leftrightarrow (x \in y ⟼ g (x)) (z) \in z)$
44	43	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))$
45	44	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))$
46	41 45	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)))$
47	46	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)))$
48	20 40 47	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))$
49	48	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))$
50	8 19 49	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))$
51	50	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))$
52		dfac4	$⊢ CHOICE \leftrightarrow \forall y \exists f (f Fn y \land \forall z \in y (z \neq \emptyset \to f (z) \in z))$
53	51 52	sylibr	$⊢ \forall x \underline{AC} x = V \to CHOICE$
54	3 53	impbii	$⊢ CHOICE \leftrightarrow \forall x \underline{AC} x = V$

Metamath Proof Explorer

Theorem dfacacn

Proof