Theorem fineqvac 35833

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 35834. (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 3934	. . . . . . 7 ⊢ (𝑥 = ∅ → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ ∅))
5		dmeq 5884	. . . . . . . 8 ⊢ (𝑥 = ∅ → dom 𝑥 = dom ∅)
6	5	fneq2d 6633	. . . . . . 7 ⊢ (𝑥 = ∅ → (𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom ∅))
7	4, 6	anbi12d 644	. . . . . 6 ⊢ (𝑥 = ∅ → ((𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ (𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅)))
8	7	exbidv 1953	. . . . 5 ⊢ (𝑥 = ∅ → (∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ ∃𝑓(𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅)))
9		sseq2 3934	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ 𝑦))
10		dmeq 5884	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → dom 𝑥 = dom 𝑦)
11	10	fneq2d 6633	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom 𝑦))
12	9, 11	anbi12d 644	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ (𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦)))
13	12	exbidv 1953	. . . . 5 ⊢ (𝑥 = 𝑦 → (∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ ∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦)))
14		sseq2 3934	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ (𝑦 ∪ {𝑧})))
15		dmeq 5884	. . . . . . . 8 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → dom 𝑥 = dom (𝑦 ∪ {𝑧}))
16	15	fneq2d 6633	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
17	14, 16	anbi12d 644	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ (𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))))
18	17	exbidv 1953	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))))
19		sseq2 3934	. . . . . . 7 ⊢ (𝑥 = 𝑤 → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ 𝑤))
20		dmeq 5884	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → dom 𝑥 = dom 𝑤)
21	20	fneq2d 6633	. . . . . . 7 ⊢ (𝑥 = 𝑤 → (𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom 𝑤))
22	19, 21	anbi12d 644	. . . . . 6 ⊢ (𝑥 = 𝑤 → ((𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ (𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤)))
23	22	exbidv 1953	. . . . 5 ⊢ (𝑥 = 𝑤 → (∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ ∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤)))
24		ssid 3930	. . . . . 6 ⊢ ∅ ⊆ ∅
25		fun0 6605	. . . . . . 7 ⊢ Fun ∅
26		funfn 6570	. . . . . . 7 ⊢ (Fun ∅ ↔ ∅ Fn dom ∅)
27	25, 26	mpbi 233	. . . . . 6 ⊢ ∅ Fn dom ∅
28		0ex 5260	. . . . . . 7 ⊢ ∅ ∈ V
29		sseq1 3933	. . . . . . . 8 ⊢ (𝑓 = ∅ → (𝑓 ⊆ ∅ ↔ ∅ ⊆ ∅))
30		fneq1 6630	. . . . . . . 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 3933	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (𝑓 ⊆ 𝑦 ↔ 𝑔 ⊆ 𝑦))
35		fneq1 6630	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (𝑓 Fn dom 𝑦 ↔ 𝑔 Fn dom 𝑦))
36	34, 35	anbi12d 644	. . . . . . . 8 ⊢ (𝑓 = 𝑔 → ((𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) ↔ (𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦)))
37	36	cbvexvw 2069	. . . . . . 7 ⊢ (∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) ↔ ∃𝑔(𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦))
38		ssun3 4178	. . . . . . . . . . 11 ⊢ (𝑔 ⊆ 𝑦 → 𝑔 ⊆ (𝑦 ∪ {𝑧}))
39	38	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} = ∅) → 𝑔 ⊆ (𝑦 ∪ {𝑧}))
40		dmun 5891	. . . . . . . . . . . . . 14 ⊢ dom (𝑦 ∪ {𝑧}) = (dom 𝑦 ∪ dom {𝑧})
41		uneq2 4161	. . . . . . . . . . . . . . 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 6633	. . . . . . . . . . . 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 3933	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → (𝑓 ⊆ (𝑦 ∪ {𝑧}) ↔ 𝑔 ⊆ (𝑦 ∪ {𝑧})))
50		fneq1 6630	. . . . . . . . . . . 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 6208	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (V × V) ↔ dom {𝑧} ≠ ∅)
55		elvv 5725	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (V × V) ↔ ∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
56	54, 55	bitr3i 280	. . . . . . . . . . . 12 ⊢ (dom {𝑧} ≠ ∅ ↔ ∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
57	56	anbi2i 635	. . . . . . . . . . 11 ⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} ≠ ∅) ↔ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ ∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩))
58		19.42vv 1989	. . . . . . . . . . 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 4187	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑢} ⊆ dom 𝑦 ↔ (dom 𝑦 ∪ {𝑢}) = dom 𝑦)
63	61, 62	sylib 221	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ dom 𝑦 → (dom 𝑦 ∪ {𝑢}) = dom 𝑦)
64	63	fneq2d 6633	. . . . . . . . . . . . . . . . . . 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 5886	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → dom {𝑧} = dom {⟨𝑢, 𝑣⟩})
69		vex 3454	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑣 ∈ V
70	69	dmsnop 6217	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ dom {⟨𝑢, 𝑣⟩} = {𝑢}
71	68, 70	eqtrdi 2811	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → dom {𝑧} = {𝑢})
72	71	uneq2d 4167	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → (dom 𝑦 ∪ dom {𝑧}) = (dom 𝑦 ∪ {𝑢}))
73	40, 72	eqtrid 2807	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → dom (𝑦 ∪ {𝑧}) = (dom 𝑦 ∪ {𝑢}))
74	73	fneq2d 6633	. . . . . . . . . . . . . . . . . 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 4167	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → (𝑔 ∪ {𝑧}) = (𝑔 ∪ {⟨𝑢, 𝑣⟩}))
81	80	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑔 ∪ {𝑧}) = (𝑔 ∪ {⟨𝑢, 𝑣⟩}))
82		unss1 4183	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ⊆ 𝑦 → (𝑔 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
83	82	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑔 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
84	81, 83	eqsstrrd 3943	. . . . . . . . . . . . . . 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 6655	. . . . . . . . . . . . . . . . 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 6633	. . . . . . . . . . . . . . . 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 7761	. . . . . . . . . . . . . . 15 ⊢ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) ∈ V
101		sseq1 3933	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑔 ∪ {⟨𝑢, 𝑣⟩}) → (𝑓 ⊆ (𝑦 ∪ {𝑧}) ↔ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) ⊆ (𝑦 ∪ {𝑧})))
102		fneq1 6630	. . . . . . . . . . . . . . . 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 1964	. . . . . . . . . 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 1962	. . . . . . 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 9181	. . . 4 ⊢ (𝑤 ∈ Fin → ∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤))
115	3, 114	syl 18	. . 3 ⊢ (Fin = V → ∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤))
116	115	alrimiv 1959	. 2 ⊢ (Fin = V → ∀𝑤∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤))
117		df-ac 10196	. 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 1567   = wceq 1569  ∃wex 1811   ∈ wcel 2144   ≠ wne 2955  Vcvv 3450   ⊆ wss 3895   ∪ cun 4149  ∅c0 4278  {csn 4583  ⟨cop 4589   × cxp 5648  dom cdm 5650  Fun wfun 6532   Fn wfn 6533  Fincfn 8974  CHOICEwac 10195

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  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-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  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 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-om 7878  df-en 8975  df-fin 8978  df-ac 10196

This theorem is used by: (None)