Theorem fineqvac 35709

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

Assertion

Ref	Expression
fineqvac	⊢ (Fin = V → CHOICE)

Proof of Theorem fineqvac

Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑓 𝑔 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3454	. . . . 5 ⊢ 𝑤 ∈ V
2		eleq2w2 2756	. . . . 5 ⊢ (Fin = V → (𝑤 ∈ Fin ↔ 𝑤 ∈ V))
3	1, 2	mpbiri 261	. . . 4 ⊢ (Fin = V → 𝑤 ∈ Fin)
4		sseq2 3956	. . . . . . 7 ⊢ (𝑥 = ∅ → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ ∅))
5		dmeq 5881	. . . . . . . 8 ⊢ (𝑥 = ∅ → dom 𝑥 = dom ∅)
6	5	fneq2d 6621	. . . . . . 7 ⊢ (𝑥 = ∅ → (𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom ∅))
7	4, 6	anbi12d 644	. . . . . 6 ⊢ (𝑥 = ∅ → ((𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ (𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅)))
8	7	exbidv 1954	. . . . 5 ⊢ (𝑥 = ∅ → (∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ ∃𝑓(𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅)))
9		sseq2 3956	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ 𝑦))
10		dmeq 5881	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → dom 𝑥 = dom 𝑦)
11	10	fneq2d 6621	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom 𝑦))
12	9, 11	anbi12d 644	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ (𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦)))
13	12	exbidv 1954	. . . . 5 ⊢ (𝑥 = 𝑦 → (∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ ∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦)))
14		sseq2 3956	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ (𝑦 ∪ {𝑧})))
15		dmeq 5881	. . . . . . . 8 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → dom 𝑥 = dom (𝑦 ∪ {𝑧}))
16	15	fneq2d 6621	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
17	14, 16	anbi12d 644	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ (𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))))
18	17	exbidv 1954	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))))
19		sseq2 3956	. . . . . . 7 ⊢ (𝑥 = 𝑤 → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ 𝑤))
20		dmeq 5881	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → dom 𝑥 = dom 𝑤)
21	20	fneq2d 6621	. . . . . . 7 ⊢ (𝑥 = 𝑤 → (𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom 𝑤))
22	19, 21	anbi12d 644	. . . . . 6 ⊢ (𝑥 = 𝑤 → ((𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ (𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤)))
23	22	exbidv 1954	. . . . 5 ⊢ (𝑥 = 𝑤 → (∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ ∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤)))
24		ssid 3952	. . . . . 6 ⊢ ∅ ⊆ ∅
25		fun0 6593	. . . . . . 7 ⊢ Fun ∅
26		funfn 6558	. . . . . . 7 ⊢ (Fun ∅ ↔ ∅ Fn dom ∅)
27	25, 26	mpbi 233	. . . . . 6 ⊢ ∅ Fn dom ∅
28		0ex 5260	. . . . . . 7 ⊢ ∅ ∈ V
29		sseq1 3955	. . . . . . . 8 ⊢ (𝑓 = ∅ → (𝑓 ⊆ ∅ ↔ ∅ ⊆ ∅))
30		fneq1 6618	. . . . . . . 8 ⊢ (𝑓 = ∅ → (𝑓 Fn dom ∅ ↔ ∅ Fn dom ∅))
31	29, 30	anbi12d 644	. . . . . . 7 ⊢ (𝑓 = ∅ → ((𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅) ↔ (∅ ⊆ ∅ ∧ ∅ Fn dom ∅)))
32	28, 31	spcev 3560	. . . . . 6 ⊢ ((∅ ⊆ ∅ ∧ ∅ Fn dom ∅) → ∃𝑓(𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅))
33	24, 27, 32	mp2an 705	. . . . 5 ⊢ ∃𝑓(𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅)
34		sseq1 3955	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (𝑓 ⊆ 𝑦 ↔ 𝑔 ⊆ 𝑦))
35		fneq1 6618	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (𝑓 Fn dom 𝑦 ↔ 𝑔 Fn dom 𝑦))
36	34, 35	anbi12d 644	. . . . . . . 8 ⊢ (𝑓 = 𝑔 → ((𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) ↔ (𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦)))
37	36	cbvexvw 2070	. . . . . . 7 ⊢ (∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) ↔ ∃𝑔(𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦))
38		ssun3 4125	. . . . . . . . . . 11 ⊢ (𝑔 ⊆ 𝑦 → 𝑔 ⊆ (𝑦 ∪ {𝑧}))
39	38	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} = ∅) → 𝑔 ⊆ (𝑦 ∪ {𝑧}))
40		dmun 5888	. . . . . . . . . . . . . 14 ⊢ dom (𝑦 ∪ {𝑧}) = (dom 𝑦 ∪ dom {𝑧})
41		uneq2 4108	. . . . . . . . . . . . . . 15 ⊢ (dom {𝑧} = ∅ → (dom 𝑦 ∪ dom {𝑧}) = (dom 𝑦 ∪ ∅))
42		un0 4343	. . . . . . . . . . . . . . 15 ⊢ (dom 𝑦 ∪ ∅) = dom 𝑦
43	41, 42	eqtrdi 2811	. . . . . . . . . . . . . 14 ⊢ (dom {𝑧} = ∅ → (dom 𝑦 ∪ dom {𝑧}) = dom 𝑦)
44	40, 43	eqtrid 2807	. . . . . . . . . . . . 13 ⊢ (dom {𝑧} = ∅ → dom (𝑦 ∪ {𝑧}) = dom 𝑦)
45	44	fneq2d 6621	. . . . . . . . . . . 12 ⊢ (dom {𝑧} = ∅ → (𝑔 Fn dom (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn dom 𝑦))
46	45	biimparc 485	. . . . . . . . . . 11 ⊢ ((𝑔 Fn dom 𝑦 ∧ dom {𝑧} = ∅) → 𝑔 Fn dom (𝑦 ∪ {𝑧}))
47	46	adantll 727	. . . . . . . . . 10 ⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} = ∅) → 𝑔 Fn dom (𝑦 ∪ {𝑧}))
48		vex 3454	. . . . . . . . . . 11 ⊢ 𝑔 ∈ V
49		sseq1 3955	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → (𝑓 ⊆ (𝑦 ∪ {𝑧}) ↔ 𝑔 ⊆ (𝑦 ∪ {𝑧})))
50		fneq1 6618	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → (𝑓 Fn dom (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn dom (𝑦 ∪ {𝑧})))
51	49, 50	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → ((𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})) ↔ (𝑔 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑔 Fn dom (𝑦 ∪ {𝑧}))))
52	48, 51	spcev 3560	. . . . . . . . . 10 ⊢ ((𝑔 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑔 Fn dom (𝑦 ∪ {𝑧})) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
53	39, 47, 52	syl2anc 596	. . . . . . . . 9 ⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} = ∅) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
54		dmsnn0 6197	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (V × V) ↔ dom {𝑧} ≠ ∅)
55		elvv 5722	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (V × V) ↔ ∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
56	54, 55	bitr3i 280	. . . . . . . . . . . 12 ⊢ (dom {𝑧} ≠ ∅ ↔ ∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
57	56	anbi2i 635	. . . . . . . . . . 11 ⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} ≠ ∅) ↔ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ ∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩))
58		19.42vv 1990	. . . . . . . . . . 11 ⊢ (∃𝑢∃𝑣((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ 𝑧 = ⟨𝑢, 𝑣⟩) ↔ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ ∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩))
59	57, 58	bitr4i 281	. . . . . . . . . 10 ⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} ≠ ∅) ↔ ∃𝑢∃𝑣((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ 𝑧 = ⟨𝑢, 𝑣⟩))
60	38	3ad2ant1 1151	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → 𝑔 ⊆ (𝑦 ∪ {𝑧}))
61		snssi 4745	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ dom 𝑦 → {𝑢} ⊆ dom 𝑦)
62		ssequn2 4134	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑢} ⊆ dom 𝑦 ↔ (dom 𝑦 ∪ {𝑢}) = dom 𝑦)
63	61, 62	sylib 221	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ dom 𝑦 → (dom 𝑦 ∪ {𝑢}) = dom 𝑦)
64	63	fneq2d 6621	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ dom 𝑦 → (𝑔 Fn (dom 𝑦 ∪ {𝑢}) ↔ 𝑔 Fn dom 𝑦))
65	64	biimparc 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 Fn dom 𝑦 ∧ 𝑢 ∈ dom 𝑦) → 𝑔 Fn (dom 𝑦 ∪ {𝑢}))
66	65	3adant2 1149	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩ ∧ 𝑢 ∈ dom 𝑦) → 𝑔 Fn (dom 𝑦 ∪ {𝑢}))
67		sneq 4593	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → {𝑧} = {⟨𝑢, 𝑣⟩})
68	67	dmeqd 5883	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → dom {𝑧} = dom {⟨𝑢, 𝑣⟩})
69		vex 3454	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑣 ∈ V
70	69	dmsnop 6206	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ dom {⟨𝑢, 𝑣⟩} = {𝑢}
71	68, 70	eqtrdi 2811	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → dom {𝑧} = {𝑢})
72	71	uneq2d 4114	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → (dom 𝑦 ∪ dom {𝑧}) = (dom 𝑦 ∪ {𝑢}))
73	40, 72	eqtrid 2807	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → dom (𝑦 ∪ {𝑧}) = (dom 𝑦 ∪ {𝑢}))
74	73	fneq2d 6621	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → (𝑔 Fn dom (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn (dom 𝑦 ∪ {𝑢})))
75	74	3ad2ant2 1152	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩ ∧ 𝑢 ∈ dom 𝑦) → (𝑔 Fn dom (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn (dom 𝑦 ∪ {𝑢})))
76	66, 75	mpbird 260	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩ ∧ 𝑢 ∈ dom 𝑦) → 𝑔 Fn dom (𝑦 ∪ {𝑧}))
77	76	3expia 1139	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑢 ∈ dom 𝑦 → 𝑔 Fn dom (𝑦 ∪ {𝑧})))
78	77	3adant1 1148	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑢 ∈ dom 𝑦 → 𝑔 Fn dom (𝑦 ∪ {𝑧})))
79	60, 78, 52	syl6an 697	. . . . . . . . . . . . 13 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑢 ∈ dom 𝑦 → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))))
80	67	uneq2d 4114	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → (𝑔 ∪ {𝑧}) = (𝑔 ∪ {⟨𝑢, 𝑣⟩}))
81	80	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑔 ∪ {𝑧}) = (𝑔 ∪ {⟨𝑢, 𝑣⟩}))
82		unss1 4130	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ⊆ 𝑦 → (𝑔 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
83	82	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑔 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
84	81, 83	eqsstrrd 3965	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑔 ∪ {⟨𝑢, 𝑣⟩}) ⊆ (𝑦 ∪ {𝑧}))
85	84	3adant2 1149	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑔 ∪ {⟨𝑢, 𝑣⟩}) ⊆ (𝑦 ∪ {𝑧}))
86		vex 3454	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑢 ∈ V
87	86	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 Fn dom 𝑦 ∧ ¬ 𝑢 ∈ dom 𝑦) → 𝑢 ∈ V)
88	69	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 Fn dom 𝑦 ∧ ¬ 𝑢 ∈ dom 𝑦) → 𝑣 ∈ V)
89		simpl 488	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 Fn dom 𝑦 ∧ ¬ 𝑢 ∈ dom 𝑦) → 𝑔 Fn dom 𝑦)
90		eqid 2760	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) = (𝑔 ∪ {⟨𝑢, 𝑣⟩})
91		eqid 2760	. . . . . . . . . . . . . . . . . 18 ⊢ (dom 𝑦 ∪ {𝑢}) = (dom 𝑦 ∪ {𝑢})
92		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 Fn dom 𝑦 ∧ ¬ 𝑢 ∈ dom 𝑦) → ¬ 𝑢 ∈ dom 𝑦)
93	87, 88, 89, 90, 91, 92	fnunop 6643	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 Fn dom 𝑦 ∧ ¬ 𝑢 ∈ dom 𝑦) → (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn (dom 𝑦 ∪ {𝑢}))
94	93	ex 418	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 Fn dom 𝑦 → (¬ 𝑢 ∈ dom 𝑦 → (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn (dom 𝑦 ∪ {𝑢})))
95	94	3ad2ant2 1152	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (¬ 𝑢 ∈ dom 𝑦 → (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn (dom 𝑦 ∪ {𝑢})))
96	73	fneq2d 6621	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ((𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn dom (𝑦 ∪ {𝑧}) ↔ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn (dom 𝑦 ∪ {𝑢})))
97	96	3ad2ant3 1153	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → ((𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn dom (𝑦 ∪ {𝑧}) ↔ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn (dom 𝑦 ∪ {𝑢})))
98	95, 97	sylibrd 262	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (¬ 𝑢 ∈ dom 𝑦 → (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn dom (𝑦 ∪ {𝑧})))
99		snex 5396	. . . . . . . . . . . . . . . 16 ⊢ {⟨𝑢, 𝑣⟩} ∈ V
100	48, 99	unex 7744	. . . . . . . . . . . . . . 15 ⊢ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) ∈ V
101		sseq1 3955	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑔 ∪ {⟨𝑢, 𝑣⟩}) → (𝑓 ⊆ (𝑦 ∪ {𝑧}) ↔ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) ⊆ (𝑦 ∪ {𝑧})))
102		fneq1 6618	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑔 ∪ {⟨𝑢, 𝑣⟩}) → (𝑓 Fn dom (𝑦 ∪ {𝑧}) ↔ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn dom (𝑦 ∪ {𝑧})))
103	101, 102	anbi12d 644	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑔 ∪ {⟨𝑢, 𝑣⟩}) → ((𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})) ↔ ((𝑔 ∪ {⟨𝑢, 𝑣⟩}) ⊆ (𝑦 ∪ {𝑧}) ∧ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn dom (𝑦 ∪ {𝑧}))))
104	100, 103	spcev 3560	. . . . . . . . . . . . . 14 ⊢ (((𝑔 ∪ {⟨𝑢, 𝑣⟩}) ⊆ (𝑦 ∪ {𝑧}) ∧ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn dom (𝑦 ∪ {𝑧})) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
105	85, 98, 104	syl6an 697	. . . . . . . . . . . . 13 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (¬ 𝑢 ∈ dom 𝑦 → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))))
106	79, 105	pm2.61d 181	. . . . . . . . . . . 12 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
107	106	3expa 1136	. . . . . . . . . . 11 ⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
108	107	exlimivv 1965	. . . . . . . . . 10 ⊢ (∃𝑢∃𝑣((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
109	59, 108	sylbi 220	. . . . . . . . 9 ⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} ≠ ∅) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
110	53, 109	pm2.61dane 3042	. . . . . . . 8 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
111	110	exlimiv 1963	. . . . . . 7 ⊢ (∃𝑔(𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
112	37, 111	sylbi 220	. . . . . 6 ⊢ (∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
113	112	a1i 11	. . . . 5 ⊢ (𝑦 ∈ Fin → (∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))))
114	8, 13, 18, 23, 33, 113	findcard2 9158	. . . 4 ⊢ (𝑤 ∈ Fin → ∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤))
115	3, 114	syl 18	. . 3 ⊢ (Fin = V → ∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤))
116	115	alrimiv 1960	. 2 ⊢ (Fin = V → ∀𝑤∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤))
117		df-ac 10167	. 2 ⊢ (CHOICE ↔ ∀𝑤∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤))
118	116, 117	sylibr 237	1 ⊢ (Fin = V → CHOICE)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145   ≠ wne 2955  Vcvv 3450   ∪ cun 3896   ⊆ wss 3898  ∅c0 4278  {csn 4583  ⟨cop 4589   × cxp 5645  dom cdm 5647  Fun wfun 6521   Fn wfn 6522  Fincfn 8951  CHOICEwac 10166

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-tr 5212  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-ord 6354  df-on 6355  df-lim 6356  df-suc 6357  df-iota 6483  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-om 7861  df-en 8952  df-fin 8955  df-ac 10167

This theorem is used by: (None)