Theorem fineqvac 35090

Description: If the Axiom of Infinity is negated, then the Axiom of Choice becomes redundant. For a shorter proof using ax-rep 5285 and ax-pow 5371, see fineqvacALT 35091. (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 3482	. . . . 5 ⊢ 𝑤 ∈ V
2		eleq2w2 2731	. . . . 5 ⊢ (Fin = V → (𝑤 ∈ Fin ↔ 𝑤 ∈ V))
3	1, 2	mpbiri 258	. . . 4 ⊢ (Fin = V → 𝑤 ∈ Fin)
4		sseq2 4022	. . . . . . 7 ⊢ (𝑥 = ∅ → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ ∅))
5		dmeq 5917	. . . . . . . 8 ⊢ (𝑥 = ∅ → dom 𝑥 = dom ∅)
6	5	fneq2d 6663	. . . . . . 7 ⊢ (𝑥 = ∅ → (𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom ∅))
7	4, 6	anbi12d 632	. . . . . 6 ⊢ (𝑥 = ∅ → ((𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ (𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅)))
8	7	exbidv 1919	. . . . 5 ⊢ (𝑥 = ∅ → (∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ ∃𝑓(𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅)))
9		sseq2 4022	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ 𝑦))
10		dmeq 5917	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → dom 𝑥 = dom 𝑦)
11	10	fneq2d 6663	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom 𝑦))
12	9, 11	anbi12d 632	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ (𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦)))
13	12	exbidv 1919	. . . . 5 ⊢ (𝑥 = 𝑦 → (∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ ∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦)))
14		sseq2 4022	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ (𝑦 ∪ {𝑧})))
15		dmeq 5917	. . . . . . . 8 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → dom 𝑥 = dom (𝑦 ∪ {𝑧}))
16	15	fneq2d 6663	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
17	14, 16	anbi12d 632	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ (𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))))
18	17	exbidv 1919	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))))
19		sseq2 4022	. . . . . . 7 ⊢ (𝑥 = 𝑤 → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ 𝑤))
20		dmeq 5917	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → dom 𝑥 = dom 𝑤)
21	20	fneq2d 6663	. . . . . . 7 ⊢ (𝑥 = 𝑤 → (𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom 𝑤))
22	19, 21	anbi12d 632	. . . . . 6 ⊢ (𝑥 = 𝑤 → ((𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ (𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤)))
23	22	exbidv 1919	. . . . 5 ⊢ (𝑥 = 𝑤 → (∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ ∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤)))
24		ssid 4018	. . . . . 6 ⊢ ∅ ⊆ ∅
25		fun0 6633	. . . . . . 7 ⊢ Fun ∅
26		funfn 6598	. . . . . . 7 ⊢ (Fun ∅ ↔ ∅ Fn dom ∅)
27	25, 26	mpbi 230	. . . . . 6 ⊢ ∅ Fn dom ∅
28		0ex 5313	. . . . . . 7 ⊢ ∅ ∈ V
29		sseq1 4021	. . . . . . . 8 ⊢ (𝑓 = ∅ → (𝑓 ⊆ ∅ ↔ ∅ ⊆ ∅))
30		fneq1 6660	. . . . . . . 8 ⊢ (𝑓 = ∅ → (𝑓 Fn dom ∅ ↔ ∅ Fn dom ∅))
31	29, 30	anbi12d 632	. . . . . . 7 ⊢ (𝑓 = ∅ → ((𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅) ↔ (∅ ⊆ ∅ ∧ ∅ Fn dom ∅)))
32	28, 31	spcev 3606	. . . . . 6 ⊢ ((∅ ⊆ ∅ ∧ ∅ Fn dom ∅) → ∃𝑓(𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅))
33	24, 27, 32	mp2an 692	. . . . 5 ⊢ ∃𝑓(𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅)
34		sseq1 4021	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (𝑓 ⊆ 𝑦 ↔ 𝑔 ⊆ 𝑦))
35		fneq1 6660	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (𝑓 Fn dom 𝑦 ↔ 𝑔 Fn dom 𝑦))
36	34, 35	anbi12d 632	. . . . . . . 8 ⊢ (𝑓 = 𝑔 → ((𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) ↔ (𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦)))
37	36	cbvexvw 2034	. . . . . . 7 ⊢ (∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) ↔ ∃𝑔(𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦))
38		ssun3 4190	. . . . . . . . . . 11 ⊢ (𝑔 ⊆ 𝑦 → 𝑔 ⊆ (𝑦 ∪ {𝑧}))
39	38	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} = ∅) → 𝑔 ⊆ (𝑦 ∪ {𝑧}))
40		dmun 5924	. . . . . . . . . . . . . 14 ⊢ dom (𝑦 ∪ {𝑧}) = (dom 𝑦 ∪ dom {𝑧})
41		uneq2 4172	. . . . . . . . . . . . . . 15 ⊢ (dom {𝑧} = ∅ → (dom 𝑦 ∪ dom {𝑧}) = (dom 𝑦 ∪ ∅))
42		un0 4400	. . . . . . . . . . . . . . 15 ⊢ (dom 𝑦 ∪ ∅) = dom 𝑦
43	41, 42	eqtrdi 2791	. . . . . . . . . . . . . 14 ⊢ (dom {𝑧} = ∅ → (dom 𝑦 ∪ dom {𝑧}) = dom 𝑦)
44	40, 43	eqtrid 2787	. . . . . . . . . . . . 13 ⊢ (dom {𝑧} = ∅ → dom (𝑦 ∪ {𝑧}) = dom 𝑦)
45	44	fneq2d 6663	. . . . . . . . . . . 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 3482	. . . . . . . . . . 11 ⊢ 𝑔 ∈ V
49		sseq1 4021	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → (𝑓 ⊆ (𝑦 ∪ {𝑧}) ↔ 𝑔 ⊆ (𝑦 ∪ {𝑧})))
50		fneq1 6660	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → (𝑓 Fn dom (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn dom (𝑦 ∪ {𝑧})))
51	49, 50	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → ((𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})) ↔ (𝑔 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑔 Fn dom (𝑦 ∪ {𝑧}))))
52	48, 51	spcev 3606	. . . . . . . . . 10 ⊢ ((𝑔 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑔 Fn dom (𝑦 ∪ {𝑧})) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
53	39, 47, 52	syl2anc 584	. . . . . . . . 9 ⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} = ∅) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
54		dmsnn0 6229	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (V × V) ↔ dom {𝑧} ≠ ∅)
55		elvv 5763	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (V × V) ↔ ∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
56	54, 55	bitr3i 277	. . . . . . . . . . . 12 ⊢ (dom {𝑧} ≠ ∅ ↔ ∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
57	56	anbi2i 623	. . . . . . . . . . 11 ⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} ≠ ∅) ↔ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ ∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩))
58		19.42vv 1955	. . . . . . . . . . 11 ⊢ (∃𝑢∃𝑣((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ 𝑧 = ⟨𝑢, 𝑣⟩) ↔ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ ∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩))
59	57, 58	bitr4i 278	. . . . . . . . . 10 ⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} ≠ ∅) ↔ ∃𝑢∃𝑣((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ 𝑧 = ⟨𝑢, 𝑣⟩))
60	38	3ad2ant1 1132	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → 𝑔 ⊆ (𝑦 ∪ {𝑧}))
61		snssi 4813	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ dom 𝑦 → {𝑢} ⊆ dom 𝑦)
62		ssequn2 4199	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑢} ⊆ dom 𝑦 ↔ (dom 𝑦 ∪ {𝑢}) = dom 𝑦)
63	61, 62	sylib 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ dom 𝑦 → (dom 𝑦 ∪ {𝑢}) = dom 𝑦)
64	63	fneq2d 6663	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ dom 𝑦 → (𝑔 Fn (dom 𝑦 ∪ {𝑢}) ↔ 𝑔 Fn dom 𝑦))
65	64	biimparc 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 Fn dom 𝑦 ∧ 𝑢 ∈ dom 𝑦) → 𝑔 Fn (dom 𝑦 ∪ {𝑢}))
66	65	3adant2 1130	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩ ∧ 𝑢 ∈ dom 𝑦) → 𝑔 Fn (dom 𝑦 ∪ {𝑢}))
67		sneq 4641	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → {𝑧} = {⟨𝑢, 𝑣⟩})
68	67	dmeqd 5919	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → dom {𝑧} = dom {⟨𝑢, 𝑣⟩})
69		vex 3482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑣 ∈ V
70	69	dmsnop 6238	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ dom {⟨𝑢, 𝑣⟩} = {𝑢}
71	68, 70	eqtrdi 2791	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → dom {𝑧} = {𝑢})
72	71	uneq2d 4178	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → (dom 𝑦 ∪ dom {𝑧}) = (dom 𝑦 ∪ {𝑢}))
73	40, 72	eqtrid 2787	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → dom (𝑦 ∪ {𝑧}) = (dom 𝑦 ∪ {𝑢}))
74	73	fneq2d 6663	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → (𝑔 Fn dom (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn (dom 𝑦 ∪ {𝑢})))
75	74	3ad2ant2 1133	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩ ∧ 𝑢 ∈ dom 𝑦) → (𝑔 Fn dom (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn (dom 𝑦 ∪ {𝑢})))
76	66, 75	mpbird 257	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩ ∧ 𝑢 ∈ dom 𝑦) → 𝑔 Fn dom (𝑦 ∪ {𝑧}))
77	76	3expia 1120	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑢 ∈ dom 𝑦 → 𝑔 Fn dom (𝑦 ∪ {𝑧})))
78	77	3adant1 1129	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑢 ∈ dom 𝑦 → 𝑔 Fn dom (𝑦 ∪ {𝑧})))
79	60, 78, 52	syl6an 684	. . . . . . . . . . . . 13 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑢 ∈ dom 𝑦 → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))))
80	67	uneq2d 4178	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → (𝑔 ∪ {𝑧}) = (𝑔 ∪ {⟨𝑢, 𝑣⟩}))
81	80	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑔 ∪ {𝑧}) = (𝑔 ∪ {⟨𝑢, 𝑣⟩}))
82		unss1 4195	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ⊆ 𝑦 → (𝑔 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
83	82	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑔 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
84	81, 83	eqsstrrd 4035	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑔 ∪ {⟨𝑢, 𝑣⟩}) ⊆ (𝑦 ∪ {𝑧}))
85	84	3adant2 1130	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑔 ∪ {⟨𝑢, 𝑣⟩}) ⊆ (𝑦 ∪ {𝑧}))
86		vex 3482	. . . . . . . . . . . . . . . . . . 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 2735	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) = (𝑔 ∪ {⟨𝑢, 𝑣⟩})
91		eqid 2735	. . . . . . . . . . . . . . . . . 18 ⊢ (dom 𝑦 ∪ {𝑢}) = (dom 𝑦 ∪ {𝑢})
92		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 Fn dom 𝑦 ∧ ¬ 𝑢 ∈ dom 𝑦) → ¬ 𝑢 ∈ dom 𝑦)
93	87, 88, 89, 90, 91, 92	fnunop 6685	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 Fn dom 𝑦 ∧ ¬ 𝑢 ∈ dom 𝑦) → (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn (dom 𝑦 ∪ {𝑢}))
94	93	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 Fn dom 𝑦 → (¬ 𝑢 ∈ dom 𝑦 → (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn (dom 𝑦 ∪ {𝑢})))
95	94	3ad2ant2 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (¬ 𝑢 ∈ dom 𝑦 → (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn (dom 𝑦 ∪ {𝑢})))
96	73	fneq2d 6663	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ((𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn dom (𝑦 ∪ {𝑧}) ↔ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn (dom 𝑦 ∪ {𝑢})))
97	96	3ad2ant3 1134	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → ((𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn dom (𝑦 ∪ {𝑧}) ↔ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn (dom 𝑦 ∪ {𝑢})))
98	95, 97	sylibrd 259	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (¬ 𝑢 ∈ dom 𝑦 → (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn dom (𝑦 ∪ {𝑧})))
99		snex 5442	. . . . . . . . . . . . . . . 16 ⊢ {⟨𝑢, 𝑣⟩} ∈ V
100	48, 99	unex 7763	. . . . . . . . . . . . . . 15 ⊢ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) ∈ V
101		sseq1 4021	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑔 ∪ {⟨𝑢, 𝑣⟩}) → (𝑓 ⊆ (𝑦 ∪ {𝑧}) ↔ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) ⊆ (𝑦 ∪ {𝑧})))
102		fneq1 6660	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑔 ∪ {⟨𝑢, 𝑣⟩}) → (𝑓 Fn dom (𝑦 ∪ {𝑧}) ↔ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn dom (𝑦 ∪ {𝑧})))
103	101, 102	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑔 ∪ {⟨𝑢, 𝑣⟩}) → ((𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})) ↔ ((𝑔 ∪ {⟨𝑢, 𝑣⟩}) ⊆ (𝑦 ∪ {𝑧}) ∧ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn dom (𝑦 ∪ {𝑧}))))
104	100, 103	spcev 3606	. . . . . . . . . . . . . 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 1117	. . . . . . . . . . 11 ⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
108	107	exlimivv 1930	. . . . . . . . . 10 ⊢ (∃𝑢∃𝑣((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
109	59, 108	sylbi 217	. . . . . . . . 9 ⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} ≠ ∅) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
110	53, 109	pm2.61dane 3027	. . . . . . . 8 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
111	110	exlimiv 1928	. . . . . . 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 9203	. . . 4 ⊢ (𝑤 ∈ Fin → ∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤))
115	3, 114	syl 17	. . 3 ⊢ (Fin = V → ∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤))
116	115	alrimiv 1925	. 2 ⊢ (Fin = V → ∀𝑤∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤))
117		df-ac 10154	. 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 1535   = wceq 1537  ∃wex 1776   ∈ wcel 2106   ≠ wne 2938  Vcvv 3478   ∪ cun 3961   ⊆ wss 3963  ∅c0 4339  {csn 4631  ⟨cop 4637   × cxp 5687  dom cdm 5689  Fun wfun 6557   Fn wfn 6558  Fincfn 8984  CHOICEwac 10153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-om 7888  df-en 8985  df-fin 8988  df-ac 10154

This theorem is referenced by: (None)