choicefi

Description: For a finite set, a choice function exists, without using the axiom of choice. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	choicefi.a	$⊢ φ \to A \in Fin$
	choicefi.b	$⊢ (φ \land x \in A) \to B \in W$
	choicefi.n	$⊢ (φ \land x \in A) \to B \neq \emptyset$
Assertion	choicefi	$⊢ φ \to \exists f (f Fn A \land \forall x \in A f (x) \in B)$

Proof

Step	Hyp	Ref	Expression
1		choicefi.a	$⊢ φ \to A \in Fin$
2		choicefi.b	$⊢ (φ \land x \in A) \to B \in W$
3		choicefi.n	$⊢ (φ \land x \in A) \to B \neq \emptyset$
4		mptfi	$⊢ A \in Fin \to (x \in A ⟼ B) \in Fin$
5		rnfi	$⊢ (x \in A ⟼ B) \in Fin \to ran (x \in A ⟼ B) \in Fin$
6		fnchoice	$⊢ ran (x \in A ⟼ B) \in Fin \to \exists g (g Fn ran (x \in A ⟼ B) \land \forall y \in ran (x \in A ⟼ B) (y \neq \emptyset \to g (y) \in y))$
7	1 4 5 6	4syl	$⊢ φ \to \exists g (g Fn ran (x \in A ⟼ B) \land \forall y \in ran (x \in A ⟼ B) (y \neq \emptyset \to g (y) \in y))$
8		simpl	$⊢ (φ \land (g Fn ran (x \in A ⟼ B) \land \forall y \in ran (x \in A ⟼ B) (y \neq \emptyset \to g (y) \in y))) \to φ$
9		simprl	$⊢ (φ \land (g Fn ran (x \in A ⟼ B) \land \forall y \in ran (x \in A ⟼ B) (y \neq \emptyset \to g (y) \in y))) \to g Fn ran (x \in A ⟼ B)$
10		nfv	$⊢ Ⅎ y φ$
11		nfra1	$⊢ Ⅎ y \forall y \in ran (x \in A ⟼ B) (y \neq \emptyset \to g (y) \in y)$
12	10 11	nfan	$⊢ Ⅎ y (φ \land \forall y \in ran (x \in A ⟼ B) (y \neq \emptyset \to g (y) \in y))$
13		rspa	$⊢ (\forall y \in ran (x \in A ⟼ B) (y \neq \emptyset \to g (y) \in y) \land y \in ran (x \in A ⟼ B)) \to (y \neq \emptyset \to g (y) \in y)$
14	13	adantll	$⊢ ((φ \land \forall y \in ran (x \in A ⟼ B) (y \neq \emptyset \to g (y) \in y)) \land y \in ran (x \in A ⟼ B)) \to (y \neq \emptyset \to g (y) \in y)$
15		vex	$⊢ y \in V$
16		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
17	16	elrnmpt	$⊢ y \in V \to (y \in ran (x \in A ⟼ B) \leftrightarrow \exists x \in A y = B)$
18	15 17	ax-mp	$⊢ y \in ran (x \in A ⟼ B) \leftrightarrow \exists x \in A y = B$
19	18	bilani	$⊢ (φ \land y \in ran (x \in A ⟼ B)) \to \exists x \in A y = B$
20		simp3	$⊢ (φ \land x \in A \land y = B) \to y = B$
21	3	3adant3	$⊢ (φ \land x \in A \land y = B) \to B \neq \emptyset$
22	20 21	eqnetrd	$⊢ (φ \land x \in A \land y = B) \to y \neq \emptyset$
23	22	3exp	$⊢ φ \to (x \in A \to (y = B \to y \neq \emptyset))$
24	23	rexlimdv	$⊢ φ \to (\exists x \in A y = B \to y \neq \emptyset)$
25	24	adantr	$⊢ (φ \land y \in ran (x \in A ⟼ B)) \to (\exists x \in A y = B \to y \neq \emptyset)$
26	19 25	mpd	$⊢ (φ \land y \in ran (x \in A ⟼ B)) \to y \neq \emptyset$
27	26	adantlr	$⊢ ((φ \land \forall y \in ran (x \in A ⟼ B) (y \neq \emptyset \to g (y) \in y)) \land y \in ran (x \in A ⟼ B)) \to y \neq \emptyset$
28		id	$⊢ (y \neq \emptyset \to g (y) \in y) \to (y \neq \emptyset \to g (y) \in y)$
29	28	imp	$⊢ ((y \neq \emptyset \to g (y) \in y) \land y \neq \emptyset) \to g (y) \in y$
30	14 27 29	syl2anc	$⊢ ((φ \land \forall y \in ran (x \in A ⟼ B) (y \neq \emptyset \to g (y) \in y)) \land y \in ran (x \in A ⟼ B)) \to g (y) \in y$
31	30	ex	$⊢ (φ \land \forall y \in ran (x \in A ⟼ B) (y \neq \emptyset \to g (y) \in y)) \to (y \in ran (x \in A ⟼ B) \to g (y) \in y)$
32	12 31	ralrimi	$⊢ (φ \land \forall y \in ran (x \in A ⟼ B) (y \neq \emptyset \to g (y) \in y)) \to \forall y \in ran (x \in A ⟼ B) g (y) \in y$
33		rsp	$⊢ \forall y \in ran (x \in A ⟼ B) g (y) \in y \to (y \in ran (x \in A ⟼ B) \to g (y) \in y)$
34	32 33	syl	$⊢ (φ \land \forall y \in ran (x \in A ⟼ B) (y \neq \emptyset \to g (y) \in y)) \to (y \in ran (x \in A ⟼ B) \to g (y) \in y)$
35	12 34	ralrimi	$⊢ (φ \land \forall y \in ran (x \in A ⟼ B) (y \neq \emptyset \to g (y) \in y)) \to \forall y \in ran (x \in A ⟼ B) g (y) \in y$
36	35	adantrl	$⊢ (φ \land (g Fn ran (x \in A ⟼ B) \land \forall y \in ran (x \in A ⟼ B) (y \neq \emptyset \to g (y) \in y))) \to \forall y \in ran (x \in A ⟼ B) g (y) \in y$
37		vex	$⊢ g \in V$
38	37	a1i	$⊢ φ \to g \in V$
39	1	mptexd	$⊢ φ \to (x \in A ⟼ B) \in V$
40		coexg	$⊢ (g \in V \land (x \in A ⟼ B) \in V) \to g \circ (x \in A ⟼ B) \in V$
41	38 39 40	syl2anc	$⊢ φ \to g \circ (x \in A ⟼ B) \in V$
42	41	3ad2ant1	$⊢ (φ \land g Fn ran (x \in A ⟼ B) \land \forall y \in ran (x \in A ⟼ B) g (y) \in y) \to g \circ (x \in A ⟼ B) \in V$
43		simpr	$⊢ (φ \land g Fn ran (x \in A ⟼ B)) \to g Fn ran (x \in A ⟼ B)$
44	2	ralrimiva	$⊢ φ \to \forall x \in A B \in W$
45	16	fnmpt	$⊢ \forall x \in A B \in W \to (x \in A ⟼ B) Fn A$
46	44 45	syl	$⊢ φ \to (x \in A ⟼ B) Fn A$
47	46	adantr	$⊢ (φ \land g Fn ran (x \in A ⟼ B)) \to (x \in A ⟼ B) Fn A$
48		ssidd	$⊢ (φ \land g Fn ran (x \in A ⟼ B)) \to ran (x \in A ⟼ B) \subseteq ran (x \in A ⟼ B)$
49		fnco	$⊢ (g Fn ran (x \in A ⟼ B) \land (x \in A ⟼ B) Fn A \land ran (x \in A ⟼ B) \subseteq ran (x \in A ⟼ B)) \to (g \circ (x \in A ⟼ B)) Fn A$
50	43 47 48 49	syl3anc	$⊢ (φ \land g Fn ran (x \in A ⟼ B)) \to (g \circ (x \in A ⟼ B)) Fn A$
51	50	3adant3	$⊢ (φ \land g Fn ran (x \in A ⟼ B) \land \forall y \in ran (x \in A ⟼ B) g (y) \in y) \to (g \circ (x \in A ⟼ B)) Fn A$
52		nfv	$⊢ Ⅎ x φ$
53		nfcv	$⊢ \underline{Ⅎ} x g$
54		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B)$
55	54	nfrn	$⊢ \underline{Ⅎ} x ran (x \in A ⟼ B)$
56	53 55	nffn	$⊢ Ⅎ x g Fn ran (x \in A ⟼ B)$
57		nfv	$⊢ Ⅎ x g (y) \in y$
58	55 57	nfralw	$⊢ Ⅎ x \forall y \in ran (x \in A ⟼ B) g (y) \in y$
59	52 56 58	nf3an	$⊢ Ⅎ x (φ \land g Fn ran (x \in A ⟼ B) \land \forall y \in ran (x \in A ⟼ B) g (y) \in y)$
60		funmpt	$⊢ Fun (x \in A ⟼ B)$
61	60	a1i	$⊢ (φ \land x \in A) \to Fun (x \in A ⟼ B)$
62		simpr	$⊢ (φ \land x \in A) \to x \in A$
63	16 2	dmmptd	$⊢ φ \to dom (x \in A ⟼ B) = A$
64	63	eqcomd	$⊢ φ \to A = dom (x \in A ⟼ B)$
65	64	adantr	$⊢ (φ \land x \in A) \to A = dom (x \in A ⟼ B)$
66	62 65	eleqtrd	$⊢ (φ \land x \in A) \to x \in dom (x \in A ⟼ B)$
67		fvco	$⊢ (Fun (x \in A ⟼ B) \land x \in dom (x \in A ⟼ B)) \to (g \circ (x \in A ⟼ B)) (x) = g ((x \in A ⟼ B) (x))$
68	61 66 67	syl2anc	$⊢ (φ \land x \in A) \to (g \circ (x \in A ⟼ B)) (x) = g ((x \in A ⟼ B) (x))$
69	16	fvmpt2	$⊢ (x \in A \land B \in W) \to (x \in A ⟼ B) (x) = B$
70	62 2 69	syl2anc	$⊢ (φ \land x \in A) \to (x \in A ⟼ B) (x) = B$
71	70	fveq2d	$⊢ (φ \land x \in A) \to g ((x \in A ⟼ B) (x)) = g (B)$
72	68 71	eqtrd	$⊢ (φ \land x \in A) \to (g \circ (x \in A ⟼ B)) (x) = g (B)$
73	72	3ad2antl1	$⊢ ((φ \land g Fn ran (x \in A ⟼ B) \land \forall y \in ran (x \in A ⟼ B) g (y) \in y) \land x \in A) \to (g \circ (x \in A ⟼ B)) (x) = g (B)$
74	16	elrnmpt1	$⊢ (x \in A \land B \in W) \to B \in ran (x \in A ⟼ B)$
75	62 2 74	syl2anc	$⊢ (φ \land x \in A) \to B \in ran (x \in A ⟼ B)$
76	75	3ad2antl1	$⊢ ((φ \land g Fn ran (x \in A ⟼ B) \land \forall y \in ran (x \in A ⟼ B) g (y) \in y) \land x \in A) \to B \in ran (x \in A ⟼ B)$
77		simpl3	$⊢ ((φ \land g Fn ran (x \in A ⟼ B) \land \forall y \in ran (x \in A ⟼ B) g (y) \in y) \land x \in A) \to \forall y \in ran (x \in A ⟼ B) g (y) \in y$
78		fveq2	$⊢ y = B \to g (y) = g (B)$
79		id	$⊢ y = B \to y = B$
80	78 79	eleq12d	$⊢ y = B \to (g (y) \in y \leftrightarrow g (B) \in B)$
81	80	rspcva	$⊢ (B \in ran (x \in A ⟼ B) \land \forall y \in ran (x \in A ⟼ B) g (y) \in y) \to g (B) \in B$
82	76 77 81	syl2anc	$⊢ ((φ \land g Fn ran (x \in A ⟼ B) \land \forall y \in ran (x \in A ⟼ B) g (y) \in y) \land x \in A) \to g (B) \in B$
83	73 82	eqeltrd	$⊢ ((φ \land g Fn ran (x \in A ⟼ B) \land \forall y \in ran (x \in A ⟼ B) g (y) \in y) \land x \in A) \to (g \circ (x \in A ⟼ B)) (x) \in B$
84	83	ex	$⊢ (φ \land g Fn ran (x \in A ⟼ B) \land \forall y \in ran (x \in A ⟼ B) g (y) \in y) \to (x \in A \to (g \circ (x \in A ⟼ B)) (x) \in B)$
85	59 84	ralrimi	$⊢ (φ \land g Fn ran (x \in A ⟼ B) \land \forall y \in ran (x \in A ⟼ B) g (y) \in y) \to \forall x \in A (g \circ (x \in A ⟼ B)) (x) \in B$
86	51 85	jca	$⊢ (φ \land g Fn ran (x \in A ⟼ B) \land \forall y \in ran (x \in A ⟼ B) g (y) \in y) \to ((g \circ (x \in A ⟼ B)) Fn A \land \forall x \in A (g \circ (x \in A ⟼ B)) (x) \in B)$
87		fneq1	$⊢ f = g \circ (x \in A ⟼ B) \to (f Fn A \leftrightarrow (g \circ (x \in A ⟼ B)) Fn A)$
88		nfcv	$⊢ \underline{Ⅎ} x f$
89	53 54	nfco	$⊢ \underline{Ⅎ} x (g \circ (x \in A ⟼ B))$
90	88 89	nfeq	$⊢ Ⅎ x f = g \circ (x \in A ⟼ B)$
91		fveq1	$⊢ f = g \circ (x \in A ⟼ B) \to f (x) = (g \circ (x \in A ⟼ B)) (x)$
92	91	eleq1d	$⊢ f = g \circ (x \in A ⟼ B) \to (f (x) \in B \leftrightarrow (g \circ (x \in A ⟼ B)) (x) \in B)$
93	90 92	ralbid	$⊢ f = g \circ (x \in A ⟼ B) \to (\forall x \in A f (x) \in B \leftrightarrow \forall x \in A (g \circ (x \in A ⟼ B)) (x) \in B)$
94	87 93	anbi12d	$⊢ f = g \circ (x \in A ⟼ B) \to ((f Fn A \land \forall x \in A f (x) \in B) \leftrightarrow ((g \circ (x \in A ⟼ B)) Fn A \land \forall x \in A (g \circ (x \in A ⟼ B)) (x) \in B))$
95	94	spcegv	$⊢ g \circ (x \in A ⟼ B) \in V \to (((g \circ (x \in A ⟼ B)) Fn A \land \forall x \in A (g \circ (x \in A ⟼ B)) (x) \in B) \to \exists f (f Fn A \land \forall x \in A f (x) \in B))$
96	42 86 95	sylc	$⊢ (φ \land g Fn ran (x \in A ⟼ B) \land \forall y \in ran (x \in A ⟼ B) g (y) \in y) \to \exists f (f Fn A \land \forall x \in A f (x) \in B)$
97	8 9 36 96	syl3anc	$⊢ (φ \land (g Fn ran (x \in A ⟼ B) \land \forall y \in ran (x \in A ⟼ B) (y \neq \emptyset \to g (y) \in y))) \to \exists f (f Fn A \land \forall x \in A f (x) \in B)$
98	97	ex	$⊢ φ \to ((g Fn ran (x \in A ⟼ B) \land \forall y \in ran (x \in A ⟼ B) (y \neq \emptyset \to g (y) \in y)) \to \exists f (f Fn A \land \forall x \in A f (x) \in B))$
99	98	exlimdv	$⊢ φ \to (\exists g (g Fn ran (x \in A ⟼ B) \land \forall y \in ran (x \in A ⟼ B) (y \neq \emptyset \to g (y) \in y)) \to \exists f (f Fn A \land \forall x \in A f (x) \in B))$
100	7 99	mpd	$⊢ φ \to \exists f (f Fn A \land \forall x \in A f (x) \in B)$

Metamath Proof Explorer

Theorem choicefi

Proof