Theorem fineqvac 32966

Description: If the Axiom of Infinity is negated, then the Axiom of Choice becomes redundant. For a shorter proof using ax-rep 5205 and ax-pow 5283, see fineqvacALT 32967. (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 3426	. . . . 5 ⊢ 𝑤 ∈ V
2		eleq2w2 2734	. . . . 5 ⊢ (Fin = V → (𝑤 ∈ Fin ↔ 𝑤 ∈ V))
3	1, 2	mpbiri 257	. . . 4 ⊢ (Fin = V → 𝑤 ∈ Fin)
4		sseq2 3943	. . . . . . 7 ⊢ (𝑥 = ∅ → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ ∅))
5		dmeq 5801	. . . . . . . 8 ⊢ (𝑥 = ∅ → dom 𝑥 = dom ∅)
6	5	fneq2d 6511	. . . . . . 7 ⊢ (𝑥 = ∅ → (𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom ∅))
7	4, 6	anbi12d 630	. . . . . 6 ⊢ (𝑥 = ∅ → ((𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ (𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅)))
8	7	exbidv 1925	. . . . 5 ⊢ (𝑥 = ∅ → (∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ ∃𝑓(𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅)))
9		sseq2 3943	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ 𝑦))
10		dmeq 5801	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → dom 𝑥 = dom 𝑦)
11	10	fneq2d 6511	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom 𝑦))
12	9, 11	anbi12d 630	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ (𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦)))
13	12	exbidv 1925	. . . . 5 ⊢ (𝑥 = 𝑦 → (∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ ∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦)))
14		sseq2 3943	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ (𝑦 ∪ {𝑧})))
15		dmeq 5801	. . . . . . . 8 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → dom 𝑥 = dom (𝑦 ∪ {𝑧}))
16	15	fneq2d 6511	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
17	14, 16	anbi12d 630	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ (𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))))
18	17	exbidv 1925	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))))
19		sseq2 3943	. . . . . . 7 ⊢ (𝑥 = 𝑤 → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ 𝑤))
20		dmeq 5801	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → dom 𝑥 = dom 𝑤)
21	20	fneq2d 6511	. . . . . . 7 ⊢ (𝑥 = 𝑤 → (𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom 𝑤))
22	19, 21	anbi12d 630	. . . . . 6 ⊢ (𝑥 = 𝑤 → ((𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ (𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤)))
23	22	exbidv 1925	. . . . 5 ⊢ (𝑥 = 𝑤 → (∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ ∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤)))
24		ssid 3939	. . . . . 6 ⊢ ∅ ⊆ ∅
25		fun0 6483	. . . . . . 7 ⊢ Fun ∅
26		funfn 6448	. . . . . . 7 ⊢ (Fun ∅ ↔ ∅ Fn dom ∅)
27	25, 26	mpbi 229	. . . . . 6 ⊢ ∅ Fn dom ∅
28		0ex 5226	. . . . . . 7 ⊢ ∅ ∈ V
29		sseq1 3942	. . . . . . . 8 ⊢ (𝑓 = ∅ → (𝑓 ⊆ ∅ ↔ ∅ ⊆ ∅))
30		fneq1 6508	. . . . . . . 8 ⊢ (𝑓 = ∅ → (𝑓 Fn dom ∅ ↔ ∅ Fn dom ∅))
31	29, 30	anbi12d 630	. . . . . . 7 ⊢ (𝑓 = ∅ → ((𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅) ↔ (∅ ⊆ ∅ ∧ ∅ Fn dom ∅)))
32	28, 31	spcev 3535	. . . . . 6 ⊢ ((∅ ⊆ ∅ ∧ ∅ Fn dom ∅) → ∃𝑓(𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅))
33	24, 27, 32	mp2an 688	. . . . 5 ⊢ ∃𝑓(𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅)
34		sseq1 3942	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (𝑓 ⊆ 𝑦 ↔ 𝑔 ⊆ 𝑦))
35		fneq1 6508	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (𝑓 Fn dom 𝑦 ↔ 𝑔 Fn dom 𝑦))
36	34, 35	anbi12d 630	. . . . . . . 8 ⊢ (𝑓 = 𝑔 → ((𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) ↔ (𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦)))
37	36	cbvexvw 2041	. . . . . . 7 ⊢ (∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) ↔ ∃𝑔(𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦))
38		ssun3 4104	. . . . . . . . . . 11 ⊢ (𝑔 ⊆ 𝑦 → 𝑔 ⊆ (𝑦 ∪ {𝑧}))
39	38	ad2antrr 722	. . . . . . . . . 10 ⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} = ∅) → 𝑔 ⊆ (𝑦 ∪ {𝑧}))
40		dmun 5808	. . . . . . . . . . . . . 14 ⊢ dom (𝑦 ∪ {𝑧}) = (dom 𝑦 ∪ dom {𝑧})
41		uneq2 4087	. . . . . . . . . . . . . . 15 ⊢ (dom {𝑧} = ∅ → (dom 𝑦 ∪ dom {𝑧}) = (dom 𝑦 ∪ ∅))
42		un0 4321	. . . . . . . . . . . . . . 15 ⊢ (dom 𝑦 ∪ ∅) = dom 𝑦
43	41, 42	eqtrdi 2795	. . . . . . . . . . . . . 14 ⊢ (dom {𝑧} = ∅ → (dom 𝑦 ∪ dom {𝑧}) = dom 𝑦)
44	40, 43	syl5eq 2791	. . . . . . . . . . . . 13 ⊢ (dom {𝑧} = ∅ → dom (𝑦 ∪ {𝑧}) = dom 𝑦)
45	44	fneq2d 6511	. . . . . . . . . . . 12 ⊢ (dom {𝑧} = ∅ → (𝑔 Fn dom (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn dom 𝑦))
46	45	biimparc 479	. . . . . . . . . . 11 ⊢ ((𝑔 Fn dom 𝑦 ∧ dom {𝑧} = ∅) → 𝑔 Fn dom (𝑦 ∪ {𝑧}))
47	46	adantll 710	. . . . . . . . . 10 ⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} = ∅) → 𝑔 Fn dom (𝑦 ∪ {𝑧}))
48		vex 3426	. . . . . . . . . . 11 ⊢ 𝑔 ∈ V
49		sseq1 3942	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → (𝑓 ⊆ (𝑦 ∪ {𝑧}) ↔ 𝑔 ⊆ (𝑦 ∪ {𝑧})))
50		fneq1 6508	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → (𝑓 Fn dom (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn dom (𝑦 ∪ {𝑧})))
51	49, 50	anbi12d 630	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → ((𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})) ↔ (𝑔 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑔 Fn dom (𝑦 ∪ {𝑧}))))
52	48, 51	spcev 3535	. . . . . . . . . 10 ⊢ ((𝑔 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑔 Fn dom (𝑦 ∪ {𝑧})) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
53	39, 47, 52	syl2anc 583	. . . . . . . . 9 ⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} = ∅) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
54		dmsnn0 6099	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (V × V) ↔ dom {𝑧} ≠ ∅)
55		elvv 5652	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (V × V) ↔ ∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
56	54, 55	bitr3i 276	. . . . . . . . . . . 12 ⊢ (dom {𝑧} ≠ ∅ ↔ ∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
57	56	anbi2i 622	. . . . . . . . . . 11 ⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} ≠ ∅) ↔ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ ∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩))
58		19.42vv 1962	. . . . . . . . . . 11 ⊢ (∃𝑢∃𝑣((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ 𝑧 = ⟨𝑢, 𝑣⟩) ↔ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ ∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩))
59	57, 58	bitr4i 277	. . . . . . . . . 10 ⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} ≠ ∅) ↔ ∃𝑢∃𝑣((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ 𝑧 = ⟨𝑢, 𝑣⟩))
60	38	3ad2ant1 1131	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → 𝑔 ⊆ (𝑦 ∪ {𝑧}))
61		snssi 4738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ dom 𝑦 → {𝑢} ⊆ dom 𝑦)
62		ssequn2 4113	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑢} ⊆ dom 𝑦 ↔ (dom 𝑦 ∪ {𝑢}) = dom 𝑦)
63	61, 62	sylib 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ dom 𝑦 → (dom 𝑦 ∪ {𝑢}) = dom 𝑦)
64	63	fneq2d 6511	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ dom 𝑦 → (𝑔 Fn (dom 𝑦 ∪ {𝑢}) ↔ 𝑔 Fn dom 𝑦))
65	64	biimparc 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 Fn dom 𝑦 ∧ 𝑢 ∈ dom 𝑦) → 𝑔 Fn (dom 𝑦 ∪ {𝑢}))
66	65	3adant2 1129	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩ ∧ 𝑢 ∈ dom 𝑦) → 𝑔 Fn (dom 𝑦 ∪ {𝑢}))
67		sneq 4568	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → {𝑧} = {⟨𝑢, 𝑣⟩})
68	67	dmeqd 5803	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → dom {𝑧} = dom {⟨𝑢, 𝑣⟩})
69		vex 3426	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑣 ∈ V
70	69	dmsnop 6108	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ dom {⟨𝑢, 𝑣⟩} = {𝑢}
71	68, 70	eqtrdi 2795	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → dom {𝑧} = {𝑢})
72	71	uneq2d 4093	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → (dom 𝑦 ∪ dom {𝑧}) = (dom 𝑦 ∪ {𝑢}))
73	40, 72	syl5eq 2791	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → dom (𝑦 ∪ {𝑧}) = (dom 𝑦 ∪ {𝑢}))
74	73	fneq2d 6511	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → (𝑔 Fn dom (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn (dom 𝑦 ∪ {𝑢})))
75	74	3ad2ant2 1132	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩ ∧ 𝑢 ∈ dom 𝑦) → (𝑔 Fn dom (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn (dom 𝑦 ∪ {𝑢})))
76	66, 75	mpbird 256	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩ ∧ 𝑢 ∈ dom 𝑦) → 𝑔 Fn dom (𝑦 ∪ {𝑧}))
77	76	3expia 1119	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑢 ∈ dom 𝑦 → 𝑔 Fn dom (𝑦 ∪ {𝑧})))
78	77	3adant1 1128	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑢 ∈ dom 𝑦 → 𝑔 Fn dom (𝑦 ∪ {𝑧})))
79	60, 78, 52	syl6an 680	. . . . . . . . . . . . 13 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑢 ∈ dom 𝑦 → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))))
80	67	uneq2d 4093	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → (𝑔 ∪ {𝑧}) = (𝑔 ∪ {⟨𝑢, 𝑣⟩}))
81	80	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑔 ∪ {𝑧}) = (𝑔 ∪ {⟨𝑢, 𝑣⟩}))
82		unss1 4109	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ⊆ 𝑦 → (𝑔 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
83	82	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑔 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
84	81, 83	eqsstrrd 3956	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑔 ∪ {⟨𝑢, 𝑣⟩}) ⊆ (𝑦 ∪ {𝑧}))
85	84	3adant2 1129	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑔 ∪ {⟨𝑢, 𝑣⟩}) ⊆ (𝑦 ∪ {𝑧}))
86		vex 3426	. . . . . . . . . . . . . . . . . . 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 2738	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) = (𝑔 ∪ {⟨𝑢, 𝑣⟩})
91		eqid 2738	. . . . . . . . . . . . . . . . . 18 ⊢ (dom 𝑦 ∪ {𝑢}) = (dom 𝑦 ∪ {𝑢})
92		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 Fn dom 𝑦 ∧ ¬ 𝑢 ∈ dom 𝑦) → ¬ 𝑢 ∈ dom 𝑦)
93	87, 88, 89, 90, 91, 92	fnunop 6531	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 Fn dom 𝑦 ∧ ¬ 𝑢 ∈ dom 𝑦) → (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn (dom 𝑦 ∪ {𝑢}))
94	93	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 Fn dom 𝑦 → (¬ 𝑢 ∈ dom 𝑦 → (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn (dom 𝑦 ∪ {𝑢})))
95	94	3ad2ant2 1132	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (¬ 𝑢 ∈ dom 𝑦 → (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn (dom 𝑦 ∪ {𝑢})))
96	73	fneq2d 6511	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ((𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn dom (𝑦 ∪ {𝑧}) ↔ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn (dom 𝑦 ∪ {𝑢})))
97	96	3ad2ant3 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → ((𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn dom (𝑦 ∪ {𝑧}) ↔ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn (dom 𝑦 ∪ {𝑢})))
98	95, 97	sylibrd 258	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (¬ 𝑢 ∈ dom 𝑦 → (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn dom (𝑦 ∪ {𝑧})))
99		snex 5349	. . . . . . . . . . . . . . . 16 ⊢ {⟨𝑢, 𝑣⟩} ∈ V
100	48, 99	unex 7574	. . . . . . . . . . . . . . 15 ⊢ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) ∈ V
101		sseq1 3942	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑔 ∪ {⟨𝑢, 𝑣⟩}) → (𝑓 ⊆ (𝑦 ∪ {𝑧}) ↔ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) ⊆ (𝑦 ∪ {𝑧})))
102		fneq1 6508	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑔 ∪ {⟨𝑢, 𝑣⟩}) → (𝑓 Fn dom (𝑦 ∪ {𝑧}) ↔ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn dom (𝑦 ∪ {𝑧})))
103	101, 102	anbi12d 630	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑔 ∪ {⟨𝑢, 𝑣⟩}) → ((𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})) ↔ ((𝑔 ∪ {⟨𝑢, 𝑣⟩}) ⊆ (𝑦 ∪ {𝑧}) ∧ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn dom (𝑦 ∪ {𝑧}))))
104	100, 103	spcev 3535	. . . . . . . . . . . . . 14 ⊢ (((𝑔 ∪ {⟨𝑢, 𝑣⟩}) ⊆ (𝑦 ∪ {𝑧}) ∧ (𝑔 ∪ {⟨𝑢, 𝑣⟩}) Fn dom (𝑦 ∪ {𝑧})) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
105	85, 98, 104	syl6an 680	. . . . . . . . . . . . 13 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → (¬ 𝑢 ∈ dom 𝑦 → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))))
106	79, 105	pm2.61d 179	. . . . . . . . . . . 12 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
107	106	3expa 1116	. . . . . . . . . . 11 ⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
108	107	exlimivv 1936	. . . . . . . . . 10 ⊢ (∃𝑢∃𝑣((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ 𝑧 = ⟨𝑢, 𝑣⟩) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
109	59, 108	sylbi 216	. . . . . . . . 9 ⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} ≠ ∅) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
110	53, 109	pm2.61dane 3031	. . . . . . . 8 ⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
111	110	exlimiv 1934	. . . . . . 7 ⊢ (∃𝑔(𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
112	37, 111	sylbi 216	. . . . . 6 ⊢ (∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))
113	112	a1i 11	. . . . 5 ⊢ (𝑦 ∈ Fin → (∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))))
114	8, 13, 18, 23, 33, 113	findcard2 8909	. . . 4 ⊢ (𝑤 ∈ Fin → ∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤))
115	3, 114	syl 17	. . 3 ⊢ (Fin = V → ∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤))
116	115	alrimiv 1931	. 2 ⊢ (Fin = V → ∀𝑤∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤))
117		df-ac 9803	. 2 ⊢ (CHOICE ↔ ∀𝑤∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤))
118	116, 117	sylibr 233	1 ⊢ (Fin = V → CHOICE)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085  ∀wal 1537   = wceq 1539  ∃wex 1783   ∈ wcel 2108   ≠ wne 2942  Vcvv 3422   ∪ cun 3881   ⊆ wss 3883  ∅c0 4253  {csn 4558  ⟨cop 4564   × cxp 5578  dom cdm 5580  Fun wfun 6412   Fn wfn 6413  Fincfn 8691  CHOICEwac 9802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-om 7688  df-en 8692  df-fin 8695  df-ac 9803

This theorem is referenced by: (None)