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

Metamath Proof Explorer

Theorem choicefi

Proof