Theorem fineqvac 35146

Description: If the Axiom of Infinity is negated, then the Axiom of Choice becomes redundant. For a shorter proof using ax-rep 5219 and ax-pow 5305, see fineqvacALT 35147. (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 3440	. . . . 5 ⊢ 𝑤 ∈ V
2		eleq2w2 2727	. . . . 5 ⊢ (Fin = V → (𝑤 ∈ Fin ↔ 𝑤 ∈ V))
3	1, 2	mpbiri 258	. . . 4 ⊢ (Fin = V → 𝑤 ∈ Fin)
4		sseq2 3956	. . . . . . 7 ⊢ (𝑥 = ∅ → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ ∅))
5		dmeq 5848	. . . . . . . 8 ⊢ (𝑥 = ∅ → dom 𝑥 = dom ∅)
6	5	fneq2d 6581	. . . . . . 7 ⊢ (𝑥 = ∅ → (𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom ∅))
7	4, 6	anbi12d 632	. . . . . 6 ⊢ (𝑥 = ∅ → ((𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ (𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅)))
8	7	exbidv 1922	. . . . 5 ⊢ (𝑥 = ∅ → (∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ ∃𝑓(𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅)))
9		sseq2 3956	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ 𝑦))
10		dmeq 5848	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → dom 𝑥 = dom 𝑦)
11	10	fneq2d 6581	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom 𝑦))
12	9, 11	anbi12d 632	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ (𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦)))
13	12	exbidv 1922	. . . . 5 ⊢ (𝑥 = 𝑦 → (∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ ∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦)))
14		sseq2 3956	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ (𝑦 ∪ {𝑧})))
15		dmeq 5848	. . . . . . . 8 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → dom 𝑥 = dom (𝑦 ∪ {𝑧}))
16	15	fneq2d 6581	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
17	14, 16	anbi12d 632	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ (𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))))
18	17	exbidv 1922	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))))
19		sseq2 3956	. . . . . . 7 ⊢ (𝑥 = 𝑤 → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ 𝑤))
20		dmeq 5848	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → dom 𝑥 = dom 𝑤)
21	20	fneq2d 6581	. . . . . . 7 ⊢ (𝑥 = 𝑤 → (𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom 𝑤))
22	19, 21	anbi12d 632	. . . . . 6 ⊢ (𝑥 = 𝑤 → ((𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ (𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤)))
23	22	exbidv 1922	. . . . 5 ⊢ (𝑥 = 𝑤 → (∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ ∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤)))
24		ssid 3952	. . . . . 6 ⊢ ∅ ⊆ ∅
25		fun0 6552	. . . . . . 7 ⊢ Fun ∅
26		funfn 6517	. . . . . . 7 ⊢ (Fun ∅ ↔ ∅ Fn dom ∅)
27	25, 26	mpbi 230	. . . . . 6 ⊢ ∅ Fn dom ∅
28		0ex 5247	. . . . . . 7 ⊢ ∅ ∈ V
29		sseq1 3955	. . . . . . . 8 ⊢ (𝑓 = ∅ → (𝑓 ⊆ ∅ ↔ ∅ ⊆ ∅))
30		fneq1 6578	. . . . . . . 8 ⊢ (𝑓 = ∅ → (𝑓 Fn dom ∅ ↔ ∅ Fn dom ∅))
31	29, 30	anbi12d 632	. . . . . . 7 ⊢ (𝑓 = ∅ → ((𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅) ↔ (∅ ⊆ ∅ ∧ ∅ Fn dom ∅)))
32	28, 31	spcev 3556	. . . . . 6 ⊢ ((∅ ⊆ ∅ ∧ ∅ Fn dom ∅) → ∃𝑓(𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅))
33	24, 27, 32	mp2an 692	. . . . 5 ⊢ ∃𝑓(𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅)
34		sseq1 3955	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (𝑓 ⊆ 𝑦 ↔ 𝑔 ⊆ 𝑦))
35		fneq1 6578	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (𝑓 Fn dom 𝑦 ↔ 𝑔 Fn dom 𝑦))
36	34, 35	anbi12d 632	. . . . . . . 8 ⊢ (𝑓 = 𝑔 → ((𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) ↔ (𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦)))
37	36	cbvexvw 2038	. . . . . . 7 ⊢ (∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) ↔ ∃𝑔(𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦))
38		ssun3 4129	. . . . . . . . . . 11 ⊢ (𝑔 ⊆ 𝑦 → 𝑔 ⊆ (𝑦 ∪ {𝑧}))
39	38	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} = ∅) → 𝑔 ⊆ (𝑦 ∪ {𝑧}))
40		dmun 5855	. . . . . . . . . . . . . 14 ⊢ dom (𝑦 ∪ {𝑧}) = (dom 𝑦 ∪ dom {𝑧})
41		uneq2 4111	. . . . . . . . . . . . . . 15 ⊢ (dom {𝑧} = ∅ → (dom 𝑦 ∪ dom {𝑧}) = (dom 𝑦 ∪ ∅))
42		un0 4343	. . . . . . . . . . . . . . 15 ⊢ (dom 𝑦 ∪ ∅) = dom 𝑦
43	41, 42	eqtrdi 2782	. . . . . . . . . . . . . 14 ⊢ (dom {𝑧} = ∅ → (dom 𝑦 ∪ dom {𝑧}) = dom 𝑦)
44	40, 43	eqtrid 2778	. . . . . . . . . . . . 13 ⊢ (dom {𝑧} = ∅ → dom (𝑦 ∪ {𝑧}) = dom 𝑦)
45	44	fneq2d 6581	. . . . . . . . . . . 12 ⊢ (dom {𝑧} = ∅ → (𝑔 Fn dom (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn dom 𝑦))
46	45	biimparc 479	. . . . . . . . . . 11 ⊢ ((𝑔 Fn dom 𝑦 ∧ dom {𝑧} = ∅) → 𝑔 Fn dom (𝑦 ∪ {𝑧}))
47	46	adantll 714	. . . . . . . . . 10 ⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} = ∅) → 𝑔 Fn dom (𝑦 ∪ {𝑧}))
48		vex 3440	. . . . . . . . . . 11 ⊢ 𝑔 ∈ V
49		sseq1 3955	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → (𝑓 ⊆ (𝑦 ∪ {𝑧}) ↔ 𝑔 ⊆ (𝑦 ∪ {𝑧})))
50		fneq1 6578	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → (𝑓 Fn dom (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn dom (𝑦 ∪ {𝑧})))
51	49, 50	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → ((𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})) ↔ (𝑔 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑔 Fn dom (𝑦 ∪ {𝑧}))))
52	48, 51	spcev 3556	. . . . . . . . . 10 ⊢ ((𝑔 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑔 Fn dom (𝑦 ∪ {𝑧})) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
53	39, 47, 52	syl2anc 584	. . . . . . . . 9 ⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} = ∅) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
54		dmsnn0 6160	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (V × V) ↔ dom {𝑧} ≠ ∅)
55		elvv 5694	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (V × V) ↔ ∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
56	54, 55	bitr3i 277	. . . . . . . . . . . 12 ⊢ (dom {𝑧} ≠ ∅ ↔ ∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
57	56	anbi2i 623	. . . . . . . . . . 11 ⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} ≠ ∅) ↔ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ ∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩))
58		19.42vv 1958	. . . . . . . . . . 11 ⊢ (∃𝑢∃𝑣((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ 𝑧 = ⟨𝑢, 𝑣⟩) ↔ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ ∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩))
59	57, 58	bitr4i 278	. . . . . . . . . 10 ⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} ≠ ∅) ↔ ∃𝑢∃𝑣((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ 𝑧 = ⟨𝑢, 𝑣⟩))
60	38	3ad2ant1 1133	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → 𝑔 ⊆ (𝑦 ∪ {𝑧}))
61		snssi 4759	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ dom 𝑦 → {𝑢} ⊆ dom 𝑦)
62		ssequn2 4138	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑢} ⊆ dom 𝑦 ↔ (dom 𝑦 ∪ {𝑢}) = dom 𝑦)
63	61, 62	sylib 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ dom 𝑦 → (dom 𝑦 ∪ {𝑢}) = dom 𝑦)
64	63	fneq2d 6581	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ dom 𝑦 → (𝑔 Fn (dom 𝑦 ∪ {𝑢}) ↔ 𝑔 Fn dom 𝑦))
65	64	biimparc 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 Fn dom 𝑦 ∧ 𝑢 ∈ dom 𝑦) → 𝑔 Fn (dom 𝑦 ∪ {𝑢}))
66	65	3adant2 1131	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩ ∧ 𝑢 ∈ dom 𝑦) → 𝑔 Fn (dom 𝑦 ∪ {𝑢}))
67		sneq 4585	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → {𝑧} = {⟨𝑢, 𝑣⟩})
68	67	dmeqd 5850	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → dom {𝑧} = dom {⟨𝑢, 𝑣⟩})
69		vex 3440	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑣 ∈ V
70	69	dmsnop 6169	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ dom {⟨𝑢, 𝑣⟩} = {𝑢}
71	68, 70	eqtrdi 2782	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → dom {𝑧} = {𝑢})
72	71	uneq2d 4117	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → (dom 𝑦 ∪ dom {𝑧}) = (dom 𝑦 ∪ {𝑢}))
73	40, 72	eqtrid 2778	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → dom (𝑦 ∪ {𝑧}) = (dom 𝑦 ∪ {𝑢}))
74	73	fneq2d 6581	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → (𝑔 Fn dom (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn (dom 𝑦 ∪ {𝑢})))
75	74	3ad2ant2 1134	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩ ∧ 𝑢 ∈ dom 𝑦) → (𝑔 Fn dom (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn (dom 𝑦 ∪ {𝑢})))
76	66, 75	mpbird 257	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩ ∧ 𝑢 ∈ dom 𝑦) → 𝑔 Fn dom (𝑦 ∪ {𝑧}))
77	76	3expia 1121	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑢 ∈ dom 𝑦 → 𝑔 Fn dom (𝑦 ∪ {𝑧})))
78	77	3adant1 1130	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑢 ∈ dom 𝑦 → 𝑔 Fn dom (𝑦 ∪ {𝑧})))
79	60, 78, 52	syl6an 684	. . . . . . . . . . . . 13 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑢 ∈ dom 𝑦 → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))))
80	67	uneq2d 4117	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → (𝑔 ∪ {𝑧}) = (𝑔 ∪ {⟨𝑢, 𝑣⟩}))
81	80	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑔 ∪ {𝑧}) = (𝑔 ∪ {⟨𝑢, 𝑣⟩}))
82		unss1 4134	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ⊆ 𝑦 → (𝑔 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
83	82	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑔 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
84	81, 83	eqsstrrd 3965	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑔 ∪ {⟨𝑢, 𝑣⟩}) ⊆ (𝑦 ∪ {𝑧}))
85	84	3adant2 1131	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑔 ∪ {⟨𝑢, 𝑣⟩}) ⊆ (𝑦 ∪ {𝑧}))
86		vex 3440	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑢 ∈ V
87	86	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 Fn dom 𝑦 ∧ ¬ 𝑢 ∈ dom 𝑦) → 𝑢 ∈ V)
88	69	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 Fn dom 𝑦 ∧ ¬ 𝑢 ∈ dom 𝑦) → 𝑣 ∈ V)
89		simpl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 Fn dom 𝑦 ∧ ¬ 𝑢 ∈ dom 𝑦) → 𝑔 Fn dom 𝑦)
90		eqid 2731	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) = (𝑔 ∪ {⟨𝑢, 𝑣⟩})
91		eqid 2731	. . . . . . . . . . . . . . . . . 18 ⊢ (dom 𝑦 ∪ {𝑢}) = (dom 𝑦 ∪ {𝑢})
92		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 Fn dom 𝑦 ∧ ¬ 𝑢 ∈ dom 𝑦) → ¬ 𝑢 ∈ dom 𝑦)
93	87, 88, 89, 90, 91, 92	fnunop 6603	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 Fn dom 𝑦 ∧ ¬ 𝑢 ∈ dom 𝑦) → (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn (dom 𝑦 ∪ {𝑢}))
94	93	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 Fn dom 𝑦 → (¬ 𝑢 ∈ dom 𝑦 → (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn (dom 𝑦 ∪ {𝑢})))
95	94	3ad2ant2 1134	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (¬ 𝑢 ∈ dom 𝑦 → (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn (dom 𝑦 ∪ {𝑢})))
96	73	fneq2d 6581	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ((𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn dom (𝑦 ∪ {𝑧}) ↔ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn (dom 𝑦 ∪ {𝑢})))
97	96	3ad2ant3 1135	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → ((𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn dom (𝑦 ∪ {𝑧}) ↔ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn (dom 𝑦 ∪ {𝑢})))
98	95, 97	sylibrd 259	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (¬ 𝑢 ∈ dom 𝑦 → (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn dom (𝑦 ∪ {𝑧})))
99		snex 5376	. . . . . . . . . . . . . . . 16 ⊢ {⟨𝑢, 𝑣⟩} ∈ V
100	48, 99	unex 7683	. . . . . . . . . . . . . . 15 ⊢ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) ∈ V
101		sseq1 3955	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑔 ∪ {⟨𝑢, 𝑣⟩}) → (𝑓 ⊆ (𝑦 ∪ {𝑧}) ↔ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) ⊆ (𝑦 ∪ {𝑧})))
102		fneq1 6578	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑔 ∪ {⟨𝑢, 𝑣⟩}) → (𝑓 Fn dom (𝑦 ∪ {𝑧}) ↔ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn dom (𝑦 ∪ {𝑧})))
103	101, 102	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑔 ∪ {⟨𝑢, 𝑣⟩}) → ((𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})) ↔ ((𝑔 ∪ {⟨𝑢, 𝑣⟩}) ⊆ (𝑦 ∪ {𝑧}) ∧ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn dom (𝑦 ∪ {𝑧}))))
104	100, 103	spcev 3556	. . . . . . . . . . . . . 14 ⊢ (((𝑔 ∪ {⟨𝑢, 𝑣⟩}) ⊆ (𝑦 ∪ {𝑧}) ∧ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn dom (𝑦 ∪ {𝑧})) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
105	85, 98, 104	syl6an 684	. . . . . . . . . . . . 13 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (¬ 𝑢 ∈ dom 𝑦 → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))))
106	79, 105	pm2.61d 179	. . . . . . . . . . . 12 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
107	106	3expa 1118	. . . . . . . . . . 11 ⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
108	107	exlimivv 1933	. . . . . . . . . 10 ⊢ (∃𝑢∃𝑣((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
109	59, 108	sylbi 217	. . . . . . . . 9 ⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} ≠ ∅) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
110	53, 109	pm2.61dane 3015	. . . . . . . 8 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
111	110	exlimiv 1931	. . . . . . 7 ⊢ (∃𝑔(𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
112	37, 111	sylbi 217	. . . . . 6 ⊢ (∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
113	112	a1i 11	. . . . 5 ⊢ (𝑦 ∈ Fin → (∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))))
114	8, 13, 18, 23, 33, 113	findcard2 9080	. . . 4 ⊢ (𝑤 ∈ Fin → ∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤))
115	3, 114	syl 17	. . 3 ⊢ (Fin = V → ∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤))
116	115	alrimiv 1928	. 2 ⊢ (Fin = V → ∀𝑤∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤))
117		df-ac 10013	. 2 ⊢ (CHOICE ↔ ∀𝑤∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤))
118	116, 117	sylibr 234	1 ⊢ (Fin = V → CHOICE)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086  ∀wal 1539   = wceq 1541  ∃wex 1780   ∈ wcel 2111   ≠ wne 2928  Vcvv 3436   ∪ cun 3895   ⊆ wss 3897  ∅c0 4282  {csn 4575  ⟨cop 4581   × cxp 5617  dom cdm 5619  Fun wfun 6481   Fn wfn 6482  Fincfn 8875  CHOICEwac 10012

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pr 5372  ax-un 7674

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-tr 5201  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-ord 6315  df-on 6316  df-lim 6317  df-suc 6318  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-f1 6492  df-fo 6493  df-f1o 6494  df-fv 6495  df-om 7803  df-en 8876  df-fin 8879  df-ac 10013

This theorem is referenced by: (None)