fineqvac

Description: If all sets are finite, then the Axiom of Choice becomes redundant. For a shorter proof using ax-rep and ax-pow , see fineqvacALT . (Contributed by BTernaryTau, 21-Sep-2024)

		Ref	Expression
	Assertion	fineqvac	$⊢ Fin = V \to CHOICE$

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ w \in V$
2		eleq2w2	$⊢ Fin = V \to (w \in Fin \leftrightarrow w \in V)$
3	1 2	mpbiri	$⊢ Fin = V \to w \in Fin$
4		sseq2	$⊢ x = \emptyset \to (f \subseteq x \leftrightarrow f \subseteq \emptyset)$
5		dmeq	$⊢ x = \emptyset \to dom x = dom \emptyset$
6	5	fneq2d	$⊢ x = \emptyset \to (f Fn dom x \leftrightarrow f Fn dom \emptyset)$
7	4 6	anbi12d	$⊢ x = \emptyset \to ((f \subseteq x \land f Fn dom x) \leftrightarrow (f \subseteq \emptyset \land f Fn dom \emptyset))$
8	7	exbidv	$⊢ x = \emptyset \to (\exists f (f \subseteq x \land f Fn dom x) \leftrightarrow \exists f (f \subseteq \emptyset \land f Fn dom \emptyset))$
9		sseq2	$⊢ x = y \to (f \subseteq x \leftrightarrow f \subseteq y)$
10		dmeq	$⊢ x = y \to dom x = dom y$
11	10	fneq2d	$⊢ x = y \to (f Fn dom x \leftrightarrow f Fn dom y)$
12	9 11	anbi12d	$⊢ x = y \to ((f \subseteq x \land f Fn dom x) \leftrightarrow (f \subseteq y \land f Fn dom y))$
13	12	exbidv	$⊢ x = y \to (\exists f (f \subseteq x \land f Fn dom x) \leftrightarrow \exists f (f \subseteq y \land f Fn dom y))$
14		sseq2	$⊢ x = y \cup \{z\} \to (f \subseteq x \leftrightarrow f \subseteq y \cup \{z\})$
15		dmeq	$⊢ x = y \cup \{z\} \to dom x = dom (y \cup \{z\})$
16	15	fneq2d	$⊢ x = y \cup \{z\} \to (f Fn dom x \leftrightarrow f Fn dom (y \cup \{z\}))$
17	14 16	anbi12d	$⊢ x = y \cup \{z\} \to ((f \subseteq x \land f Fn dom x) \leftrightarrow (f \subseteq y \cup \{z\} \land f Fn dom (y \cup \{z\})))$
18	17	exbidv	$⊢ x = y \cup \{z\} \to (\exists f (f \subseteq x \land f Fn dom x) \leftrightarrow \exists f (f \subseteq y \cup \{z\} \land f Fn dom (y \cup \{z\})))$
19		sseq2	$⊢ x = w \to (f \subseteq x \leftrightarrow f \subseteq w)$
20		dmeq	$⊢ x = w \to dom x = dom w$
21	20	fneq2d	$⊢ x = w \to (f Fn dom x \leftrightarrow f Fn dom w)$
22	19 21	anbi12d	$⊢ x = w \to ((f \subseteq x \land f Fn dom x) \leftrightarrow (f \subseteq w \land f Fn dom w))$
23	22	exbidv	$⊢ x = w \to (\exists f (f \subseteq x \land f Fn dom x) \leftrightarrow \exists f (f \subseteq w \land f Fn dom w))$
24		ssid	$⊢ \emptyset \subseteq \emptyset$
25		fun0	$⊢ Fun \emptyset$
26		funfn	$⊢ Fun \emptyset \leftrightarrow \emptyset Fn dom \emptyset$
27	25 26	mpbi	$⊢ \emptyset Fn dom \emptyset$
28		0ex	$⊢ \emptyset \in V$
29		sseq1	$⊢ f = \emptyset \to (f \subseteq \emptyset \leftrightarrow \emptyset \subseteq \emptyset)$
30		fneq1	$⊢ f = \emptyset \to (f Fn dom \emptyset \leftrightarrow \emptyset Fn dom \emptyset)$
31	29 30	anbi12d	$⊢ f = \emptyset \to ((f \subseteq \emptyset \land f Fn dom \emptyset) \leftrightarrow (\emptyset \subseteq \emptyset \land \emptyset Fn dom \emptyset))$
32	28 31	spcev	$⊢ (\emptyset \subseteq \emptyset \land \emptyset Fn dom \emptyset) \to \exists f (f \subseteq \emptyset \land f Fn dom \emptyset)$
33	24 27 32	mp2an	$⊢ \exists f (f \subseteq \emptyset \land f Fn dom \emptyset)$
34		sseq1	$⊢ f = g \to (f \subseteq y \leftrightarrow g \subseteq y)$
35		fneq1	$⊢ f = g \to (f Fn dom y \leftrightarrow g Fn dom y)$
36	34 35	anbi12d	$⊢ f = g \to ((f \subseteq y \land f Fn dom y) \leftrightarrow (g \subseteq y \land g Fn dom y))$
37	36	cbvexvw	$⊢ \exists f (f \subseteq y \land f Fn dom y) \leftrightarrow \exists g (g \subseteq y \land g Fn dom y)$
38		ssun3	$⊢ g \subseteq y \to g \subseteq y \cup \{z\}$
39	38	ad2antrr	$⊢ ((g \subseteq y \land g Fn dom y) \land dom \{z\} = \emptyset) \to g \subseteq y \cup \{z\}$
40		dmun	$⊢ dom (y \cup \{z\}) = dom y \cup dom \{z\}$
41		uneq2	$⊢ dom \{z\} = \emptyset \to dom y \cup dom \{z\} = dom y \cup \emptyset$
42		un0	$⊢ dom y \cup \emptyset = dom y$
43	41 42	eqtrdi	$⊢ dom \{z\} = \emptyset \to dom y \cup dom \{z\} = dom y$
44	40 43	eqtrid	$⊢ dom \{z\} = \emptyset \to dom (y \cup \{z\}) = dom y$
45	44	fneq2d	$⊢ dom \{z\} = \emptyset \to (g Fn dom (y \cup \{z\}) \leftrightarrow g Fn dom y)$
46	45	biimparc	$⊢ (g Fn dom y \land dom \{z\} = \emptyset) \to g Fn dom (y \cup \{z\})$
47	46	adantll	$⊢ ((g \subseteq y \land g Fn dom y) \land dom \{z\} = \emptyset) \to g Fn dom (y \cup \{z\})$
48		vex	$⊢ g \in V$
49		sseq1	$⊢ f = g \to (f \subseteq y \cup \{z\} \leftrightarrow g \subseteq y \cup \{z\})$
50		fneq1	$⊢ f = g \to (f Fn dom (y \cup \{z\}) \leftrightarrow g Fn dom (y \cup \{z\}))$
51	49 50	anbi12d	$⊢ f = g \to ((f \subseteq y \cup \{z\} \land f Fn dom (y \cup \{z\})) \leftrightarrow (g \subseteq y \cup \{z\} \land g Fn dom (y \cup \{z\})))$
52	48 51	spcev	$⊢ (g \subseteq y \cup \{z\} \land g Fn dom (y \cup \{z\})) \to \exists f (f \subseteq y \cup \{z\} \land f Fn dom (y \cup \{z\}))$
53	39 47 52	syl2anc	$⊢ ((g \subseteq y \land g Fn dom y) \land dom \{z\} = \emptyset) \to \exists f (f \subseteq y \cup \{z\} \land f Fn dom (y \cup \{z\}))$
54		dmsnn0	$⊢ z \in (V \times V) \leftrightarrow dom \{z\} \neq \emptyset$
55		elvv	$⊢ z \in (V \times V) \leftrightarrow \exists u \exists v z = ⟨u, v⟩$
56	54 55	bitr3i	$⊢ dom \{z\} \neq \emptyset \leftrightarrow \exists u \exists v z = ⟨u, v⟩$
57	56	anbi2i	$⊢ ((g \subseteq y \land g Fn dom y) \land dom \{z\} \neq \emptyset) \leftrightarrow ((g \subseteq y \land g Fn dom y) \land \exists u \exists v z = ⟨u, v⟩)$
58		19.42vv	$⊢ \exists u \exists v ((g \subseteq y \land g Fn dom y) \land z = ⟨u, v⟩) \leftrightarrow ((g \subseteq y \land g Fn dom y) \land \exists u \exists v z = ⟨u, v⟩)$
59	57 58	bitr4i	$⊢ ((g \subseteq y \land g Fn dom y) \land dom \{z\} \neq \emptyset) \leftrightarrow \exists u \exists v ((g \subseteq y \land g Fn dom y) \land z = ⟨u, v⟩)$
60	38	3ad2ant1	$⊢ (g \subseteq y \land g Fn dom y \land z = ⟨u, v⟩) \to g \subseteq y \cup \{z\}$
61		snssi	$⊢ u \in dom y \to \{u\} \subseteq dom y$
62		ssequn2	$⊢ \{u\} \subseteq dom y \leftrightarrow dom y \cup \{u\} = dom y$
63	61 62	sylib	$⊢ u \in dom y \to dom y \cup \{u\} = dom y$
64	63	fneq2d	$⊢ u \in dom y \to (g Fn (dom y \cup \{u\}) \leftrightarrow g Fn dom y)$
65	64	biimparc	$⊢ (g Fn dom y \land u \in dom y) \to g Fn (dom y \cup \{u\})$
66	65	3adant2	$⊢ (g Fn dom y \land z = ⟨u, v⟩ \land u \in dom y) \to g Fn (dom y \cup \{u\})$
67		sneq	$⊢ z = ⟨u, v⟩ \to \{z\} = \{⟨u, v⟩\}$
68	67	dmeqd	$⊢ z = ⟨u, v⟩ \to dom \{z\} = dom \{⟨u, v⟩\}$
69		vex	$⊢ v \in V$
70	69	dmsnop	$⊢ dom \{⟨u, v⟩\} = \{u\}$
71	68 70	eqtrdi	$⊢ z = ⟨u, v⟩ \to dom \{z\} = \{u\}$
72	71	uneq2d	$⊢ z = ⟨u, v⟩ \to dom y \cup dom \{z\} = dom y \cup \{u\}$
73	40 72	eqtrid	$⊢ z = ⟨u, v⟩ \to dom (y \cup \{z\}) = dom y \cup \{u\}$
74	73	fneq2d	$⊢ z = ⟨u, v⟩ \to (g Fn dom (y \cup \{z\}) \leftrightarrow g Fn (dom y \cup \{u\}))$
75	74	3ad2ant2	$⊢ (g Fn dom y \land z = ⟨u, v⟩ \land u \in dom y) \to (g Fn dom (y \cup \{z\}) \leftrightarrow g Fn (dom y \cup \{u\}))$
76	66 75	mpbird	$⊢ (g Fn dom y \land z = ⟨u, v⟩ \land u \in dom y) \to g Fn dom (y \cup \{z\})$
77	76	3expia	$⊢ (g Fn dom y \land z = ⟨u, v⟩) \to (u \in dom y \to g Fn dom (y \cup \{z\}))$
78	77	3adant1	$⊢ (g \subseteq y \land g Fn dom y \land z = ⟨u, v⟩) \to (u \in dom y \to g Fn dom (y \cup \{z\}))$
79	60 78 52	syl6an	$⊢ (g \subseteq y \land g Fn dom y \land z = ⟨u, v⟩) \to (u \in dom y \to \exists f (f \subseteq y \cup \{z\} \land f Fn dom (y \cup \{z\})))$
80	67	uneq2d	$⊢ z = ⟨u, v⟩ \to g \cup \{z\} = g \cup \{⟨u, v⟩\}$
81	80	adantl	$⊢ (g \subseteq y \land z = ⟨u, v⟩) \to g \cup \{z\} = g \cup \{⟨u, v⟩\}$
82		unss1	$⊢ g \subseteq y \to g \cup \{z\} \subseteq y \cup \{z\}$
83	82	adantr	$⊢ (g \subseteq y \land z = ⟨u, v⟩) \to g \cup \{z\} \subseteq y \cup \{z\}$
84	81 83	eqsstrrd	$⊢ (g \subseteq y \land z = ⟨u, v⟩) \to g \cup \{⟨u, v⟩\} \subseteq y \cup \{z\}$
85	84	3adant2	$⊢ (g \subseteq y \land g Fn dom y \land z = ⟨u, v⟩) \to g \cup \{⟨u, v⟩\} \subseteq y \cup \{z\}$
86		vex	$⊢ u \in V$
87	86	a1i	$⊢ (g Fn dom y \land \neg u \in dom y) \to u \in V$
88	69	a1i	$⊢ (g Fn dom y \land \neg u \in dom y) \to v \in V$
89		simpl	$⊢ (g Fn dom y \land \neg u \in dom y) \to g Fn dom y$
90		eqid	$⊢ g \cup \{⟨u, v⟩\} = g \cup \{⟨u, v⟩\}$
91		eqid	$⊢ dom y \cup \{u\} = dom y \cup \{u\}$
92		simpr	$⊢ (g Fn dom y \land \neg u \in dom y) \to \neg u \in dom y$
93	87 88 89 90 91 92	fnunop	$⊢ (g Fn dom y \land \neg u \in dom y) \to (g \cup \{⟨u, v⟩\}) Fn (dom y \cup \{u\})$
94	93	ex	$⊢ g Fn dom y \to (\neg u \in dom y \to (g \cup \{⟨u, v⟩\}) Fn (dom y \cup \{u\}))$
95	94	3ad2ant2	$⊢ (g \subseteq y \land g Fn dom y \land z = ⟨u, v⟩) \to (\neg u \in dom y \to (g \cup \{⟨u, v⟩\}) Fn (dom y \cup \{u\}))$
96	73	fneq2d	$⊢ z = ⟨u, v⟩ \to ((g \cup \{⟨u, v⟩\}) Fn dom (y \cup \{z\}) \leftrightarrow (g \cup \{⟨u, v⟩\}) Fn (dom y \cup \{u\}))$
97	96	3ad2ant3	$⊢ (g \subseteq y \land g Fn dom y \land z = ⟨u, v⟩) \to ((g \cup \{⟨u, v⟩\}) Fn dom (y \cup \{z\}) \leftrightarrow (g \cup \{⟨u, v⟩\}) Fn (dom y \cup \{u\}))$
98	95 97	sylibrd	$⊢ (g \subseteq y \land g Fn dom y \land z = ⟨u, v⟩) \to (\neg u \in dom y \to (g \cup \{⟨u, v⟩\}) Fn dom (y \cup \{z\}))$
99		snex	$⊢ \{⟨u, v⟩\} \in V$
100	48 99	unex	$⊢ g \cup \{⟨u, v⟩\} \in V$
101		sseq1	$⊢ f = g \cup \{⟨u, v⟩\} \to (f \subseteq y \cup \{z\} \leftrightarrow g \cup \{⟨u, v⟩\} \subseteq y \cup \{z\})$
102		fneq1	$⊢ f = g \cup \{⟨u, v⟩\} \to (f Fn dom (y \cup \{z\}) \leftrightarrow (g \cup \{⟨u, v⟩\}) Fn dom (y \cup \{z\}))$
103	101 102	anbi12d	$⊢ f = g \cup \{⟨u, v⟩\} \to ((f \subseteq y \cup \{z\} \land f Fn dom (y \cup \{z\})) \leftrightarrow (g \cup \{⟨u, v⟩\} \subseteq y \cup \{z\} \land (g \cup \{⟨u, v⟩\}) Fn dom (y \cup \{z\})))$
104	100 103	spcev	$⊢ (g \cup \{⟨u, v⟩\} \subseteq y \cup \{z\} \land (g \cup \{⟨u, v⟩\}) Fn dom (y \cup \{z\})) \to \exists f (f \subseteq y \cup \{z\} \land f Fn dom (y \cup \{z\}))$
105	85 98 104	syl6an	$⊢ (g \subseteq y \land g Fn dom y \land z = ⟨u, v⟩) \to (\neg u \in dom y \to \exists f (f \subseteq y \cup \{z\} \land f Fn dom (y \cup \{z\})))$
106	79 105	pm2.61d	$⊢ (g \subseteq y \land g Fn dom y \land z = ⟨u, v⟩) \to \exists f (f \subseteq y \cup \{z\} \land f Fn dom (y \cup \{z\}))$
107	106	3expa	$⊢ ((g \subseteq y \land g Fn dom y) \land z = ⟨u, v⟩) \to \exists f (f \subseteq y \cup \{z\} \land f Fn dom (y \cup \{z\}))$
108	107	exlimivv	$⊢ \exists u \exists v ((g \subseteq y \land g Fn dom y) \land z = ⟨u, v⟩) \to \exists f (f \subseteq y \cup \{z\} \land f Fn dom (y \cup \{z\}))$
109	59 108	sylbi	$⊢ ((g \subseteq y \land g Fn dom y) \land dom \{z\} \neq \emptyset) \to \exists f (f \subseteq y \cup \{z\} \land f Fn dom (y \cup \{z\}))$
110	53 109	pm2.61dane	$⊢ (g \subseteq y \land g Fn dom y) \to \exists f (f \subseteq y \cup \{z\} \land f Fn dom (y \cup \{z\}))$
111	110	exlimiv	$⊢ \exists g (g \subseteq y \land g Fn dom y) \to \exists f (f \subseteq y \cup \{z\} \land f Fn dom (y \cup \{z\}))$
112	37 111	sylbi	$⊢ \exists f (f \subseteq y \land f Fn dom y) \to \exists f (f \subseteq y \cup \{z\} \land f Fn dom (y \cup \{z\}))$
113	112	a1i	$⊢ y \in Fin \to (\exists f (f \subseteq y \land f Fn dom y) \to \exists f (f \subseteq y \cup \{z\} \land f Fn dom (y \cup \{z\})))$
114	8 13 18 23 33 113	findcard2	$⊢ w \in Fin \to \exists f (f \subseteq w \land f Fn dom w)$
115	3 114	syl	$⊢ Fin = V \to \exists f (f \subseteq w \land f Fn dom w)$
116	115	alrimiv	$⊢ Fin = V \to \forall w \exists f (f \subseteq w \land f Fn dom w)$
117		df-ac	$⊢ CHOICE \leftrightarrow \forall w \exists f (f \subseteq w \land f Fn dom w)$
118	116 117	sylibr	$⊢ Fin = V \to CHOICE$

Metamath Proof Explorer

Theorem fineqvac

Proof