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	biimpi	$⊢ y \in ran (x \in A ⟼ B) \to \exists x \in A y = B$
20	19	adantl	$⊢ (φ \land y \in ran (x \in A ⟼ B)) \to \exists x \in A y = B$
21		simp3	$⊢ (φ \land x \in A \land y = B) \to y = B$
22	3	3adant3	$⊢ (φ \land x \in A \land y = B) \to B \neq \emptyset$
23	21 22	eqnetrd	$⊢ (φ \land x \in A \land y = B) \to y \neq \emptyset$
24	23	3exp	$⊢ φ \to (x \in A \to (y = B \to y \neq \emptyset))$
25	24	rexlimdv	$⊢ φ \to (\exists x \in A y = B \to y \neq \emptyset)$
26	25	adantr	$⊢ (φ \land y \in ran (x \in A ⟼ B)) \to (\exists x \in A y = B \to y \neq \emptyset)$
27	20 26	mpd	$⊢ (φ \land y \in ran (x \in A ⟼ B)) \to y \neq \emptyset$
28	27	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$
29		id	$⊢ (y \neq \emptyset \to g (y) \in y) \to (y \neq \emptyset \to g (y) \in y)$
30	29	imp	$⊢ ((y \neq \emptyset \to g (y) \in y) \land y \neq \emptyset) \to g (y) \in y$
31	14 28 30	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$
32	31	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)$
33	12 32	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$
34		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)$
35	33 34	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)$
36	12 35	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$
37	36	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$
38		vex	$⊢ g \in V$
39	38	a1i	$⊢ φ \to g \in V$
40	1	mptexd	$⊢ φ \to (x \in A ⟼ B) \in V$
41		coexg	$⊢ (g \in V \land (x \in A ⟼ B) \in V) \to g \circ (x \in A ⟼ B) \in V$
42	39 40 41	syl2anc	$⊢ φ \to g \circ (x \in A ⟼ B) \in V$
43	42	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$
44		simpr	$⊢ (φ \land g Fn ran (x \in A ⟼ B)) \to g Fn ran (x \in A ⟼ B)$
45	2	ralrimiva	$⊢ φ \to \forall x \in A B \in W$
46	16	fnmpt	$⊢ \forall x \in A B \in W \to (x \in A ⟼ B) Fn A$
47	45 46	syl	$⊢ φ \to (x \in A ⟼ B) Fn A$
48	47	adantr	$⊢ (φ \land g Fn ran (x \in A ⟼ B)) \to (x \in A ⟼ B) Fn A$
49		ssidd	$⊢ (φ \land g Fn ran (x \in A ⟼ B)) \to ran (x \in A ⟼ B) \subseteq ran (x \in A ⟼ B)$
50		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$
51	44 48 49 50	syl3anc	$⊢ (φ \land g Fn ran (x \in A ⟼ B)) \to (g \circ (x \in A ⟼ B)) Fn A$
52	51	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$
53		nfv	$⊢ Ⅎ x φ$
54		nfcv	$⊢ \underline{Ⅎ} x g$
55		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B)$
56	55	nfrn	$⊢ \underline{Ⅎ} x ran (x \in A ⟼ B)$
57	54 56	nffn	$⊢ Ⅎ x g Fn ran (x \in A ⟼ B)$
58		nfv	$⊢ Ⅎ x g (y) \in y$
59	56 58	nfralw	$⊢ Ⅎ x \forall y \in ran (x \in A ⟼ B) g (y) \in y$
60	53 57 59	nf3an	$⊢ Ⅎ x (φ \land g Fn ran (x \in A ⟼ B) \land \forall y \in ran (x \in A ⟼ B) g (y) \in y)$
61		funmpt	$⊢ Fun (x \in A ⟼ B)$
62	61	a1i	$⊢ (φ \land x \in A) \to Fun (x \in A ⟼ B)$
63		simpr	$⊢ (φ \land x \in A) \to x \in A$
64	16 2	dmmptd	$⊢ φ \to dom (x \in A ⟼ B) = A$
65	64	eqcomd	$⊢ φ \to A = dom (x \in A ⟼ B)$
66	65	adantr	$⊢ (φ \land x \in A) \to A = dom (x \in A ⟼ B)$
67	63 66	eleqtrd	$⊢ (φ \land x \in A) \to x \in dom (x \in A ⟼ B)$
68		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))$
69	62 67 68	syl2anc	$⊢ (φ \land x \in A) \to (g \circ (x \in A ⟼ B)) (x) = g ((x \in A ⟼ B) (x))$
70	16	fvmpt2	$⊢ (x \in A \land B \in W) \to (x \in A ⟼ B) (x) = B$
71	63 2 70	syl2anc	$⊢ (φ \land x \in A) \to (x \in A ⟼ B) (x) = B$
72	71	fveq2d	$⊢ (φ \land x \in A) \to g ((x \in A ⟼ B) (x)) = g (B)$
73	69 72	eqtrd	$⊢ (φ \land x \in A) \to (g \circ (x \in A ⟼ B)) (x) = g (B)$
74	73	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)$
75	16	elrnmpt1	$⊢ (x \in A \land B \in W) \to B \in ran (x \in A ⟼ B)$
76	63 2 75	syl2anc	$⊢ (φ \land x \in A) \to B \in ran (x \in A ⟼ B)$
77	76	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)$
78		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$
79		fveq2	$⊢ y = B \to g (y) = g (B)$
80		id	$⊢ y = B \to y = B$
81	79 80	eleq12d	$⊢ y = B \to (g (y) \in y \leftrightarrow g (B) \in B)$
82	81	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$
83	77 78 82	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$
84	74 83	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$
85	84	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)$
86	60 85	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$
87	52 86	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)$
88		fneq1	$⊢ f = g \circ (x \in A ⟼ B) \to (f Fn A \leftrightarrow (g \circ (x \in A ⟼ B)) Fn A)$
89		nfcv	$⊢ \underline{Ⅎ} x f$
90	54 55	nfco	$⊢ \underline{Ⅎ} x (g \circ (x \in A ⟼ B))$
91	89 90	nfeq	$⊢ Ⅎ x f = g \circ (x \in A ⟼ B)$
92		fveq1	$⊢ f = g \circ (x \in A ⟼ B) \to f (x) = (g \circ (x \in A ⟼ B)) (x)$
93	92	eleq1d	$⊢ f = g \circ (x \in A ⟼ B) \to (f (x) \in B \leftrightarrow (g \circ (x \in A ⟼ B)) (x) \in B)$
94	91 93	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)$
95	88 94	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))$
96	95	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))$
97	43 87 96	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)$
98	8 9 37 97	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)$
99	98	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))$
100	99	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))$
101	7 100	mpd	$⊢ φ \to \exists f (f Fn A \land \forall x \in A f (x) \in B)$

Metamath Proof Explorer

Theorem choicefi

Proof