Theorem ac6sfi 7086

Description: Existence of a choice function for finite sets. (Contributed by Jeff Hankins, 26-Jun-2009.) (Proof shortened by Mario Carneiro, 29-Jan-2014.)

Hypothesis

Ref	Expression
ac6sfi.1	⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
ac6sfi	⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓))

Distinct variable groups:   𝑥,𝑓,𝐴   𝑦,𝑓,𝐵,𝑥   𝜑,𝑓   𝜓,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑓)   𝐴(𝑦)

Proof of Theorem ac6sfi

Dummy variables 𝑢 𝑤 𝑧 𝑔 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		raleq 2730	. . . 4 ⊢ (𝑢 = ∅ → (∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ ∅ ∃𝑦 ∈ 𝐵 𝜑))
2		feq2 5466	. . . . . 6 ⊢ (𝑢 = ∅ → (𝑓:𝑢⟶𝐵 ↔ 𝑓:∅⟶𝐵))
3		raleq 2730	. . . . . 6 ⊢ (𝑢 = ∅ → (∀𝑥 ∈ 𝑢 𝜓 ↔ ∀𝑥 ∈ ∅ 𝜓))
4	2, 3	anbi12d 473	. . . . 5 ⊢ (𝑢 = ∅ → ((𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ (𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓)))
5	4	exbidv 1873	. . . 4 ⊢ (𝑢 = ∅ → (∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓)))
6	1, 5	imbi12d 234	. . 3 ⊢ (𝑢 = ∅ → ((∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓)) ↔ (∀𝑥 ∈ ∅ ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))))
7		raleq 2730	. . . 4 ⊢ (𝑢 = 𝑤 → (∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑))
8		feq2 5466	. . . . . 6 ⊢ (𝑢 = 𝑤 → (𝑓:𝑢⟶𝐵 ↔ 𝑓:𝑤⟶𝐵))
9		raleq 2730	. . . . . 6 ⊢ (𝑢 = 𝑤 → (∀𝑥 ∈ 𝑢 𝜓 ↔ ∀𝑥 ∈ 𝑤 𝜓))
10	8, 9	anbi12d 473	. . . . 5 ⊢ (𝑢 = 𝑤 → ((𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)))
11	10	exbidv 1873	. . . 4 ⊢ (𝑢 = 𝑤 → (∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)))
12	7, 11	imbi12d 234	. . 3 ⊢ (𝑢 = 𝑤 → ((∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓)) ↔ (∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓))))
13		raleq 2730	. . . 4 ⊢ (𝑢 = (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑))
14		feq2 5466	. . . . . . 7 ⊢ (𝑢 = (𝑤 ∪ {𝑧}) → (𝑓:𝑢⟶𝐵 ↔ 𝑓:(𝑤 ∪ {𝑧})⟶𝐵))
15		raleq 2730	. . . . . . 7 ⊢ (𝑢 = (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ 𝑢 𝜓 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓))
16	14, 15	anbi12d 473	. . . . . 6 ⊢ (𝑢 = (𝑤 ∪ {𝑧}) → ((𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ (𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓)))
17	16	exbidv 1873	. . . . 5 ⊢ (𝑢 = (𝑤 ∪ {𝑧}) → (∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ ∃𝑓(𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓)))
18		feq1 5465	. . . . . . 7 ⊢ (𝑓 = 𝑔 → (𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ↔ 𝑔:(𝑤 ∪ {𝑧})⟶𝐵))
19		vex 2805	. . . . . . . . . . 11 ⊢ 𝑓 ∈ V
20		vex 2805	. . . . . . . . . . 11 ⊢ 𝑥 ∈ V
21	19, 20	fvex 5659	. . . . . . . . . 10 ⊢ (𝑓‘𝑥) ∈ V
22		ac6sfi.1	. . . . . . . . . 10 ⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓))
23	21, 22	sbcie 3066	. . . . . . . . 9 ⊢ ([(𝑓‘𝑥) / 𝑦]𝜑 ↔ 𝜓)
24		fveq1 5638	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑥) = (𝑔‘𝑥))
25	24	sbceq1d 3036	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → ([(𝑓‘𝑥) / 𝑦]𝜑 ↔ [(𝑔‘𝑥) / 𝑦]𝜑))
26	23, 25	bitr3id 194	. . . . . . . 8 ⊢ (𝑓 = 𝑔 → (𝜓 ↔ [(𝑔‘𝑥) / 𝑦]𝜑))
27	26	ralbidv 2532	. . . . . . 7 ⊢ (𝑓 = 𝑔 → (∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))
28	18, 27	anbi12d 473	. . . . . 6 ⊢ (𝑓 = 𝑔 → ((𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓) ↔ (𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))
29	28	cbvexv 1967	. . . . 5 ⊢ (∃𝑓(𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓) ↔ ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))
30	17, 29	bitrdi 196	. . . 4 ⊢ (𝑢 = (𝑤 ∪ {𝑧}) → (∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))
31	13, 30	imbi12d 234	. . 3 ⊢ (𝑢 = (𝑤 ∪ {𝑧}) → ((∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓)) ↔ (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))))
32		raleq 2730	. . . 4 ⊢ (𝑢 = 𝐴 → (∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑))
33		feq2 5466	. . . . . 6 ⊢ (𝑢 = 𝐴 → (𝑓:𝑢⟶𝐵 ↔ 𝑓:𝐴⟶𝐵))
34		raleq 2730	. . . . . 6 ⊢ (𝑢 = 𝐴 → (∀𝑥 ∈ 𝑢 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜓))
35	33, 34	anbi12d 473	. . . . 5 ⊢ (𝑢 = 𝐴 → ((𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓)))
36	35	exbidv 1873	. . . 4 ⊢ (𝑢 = 𝐴 → (∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓)))
37	32, 36	imbi12d 234	. . 3 ⊢ (𝑢 = 𝐴 → ((∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓)) ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓))))
38		f0 5527	. . . 4 ⊢ ∅:∅⟶𝐵
39		0ex 4216	. . . . 5 ⊢ ∅ ∈ V
40		ral0 3596	. . . . . . 7 ⊢ ∀𝑥 ∈ ∅ 𝜓
41	40	biantru 302	. . . . . 6 ⊢ (𝑓:∅⟶𝐵 ↔ (𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))
42		feq1 5465	. . . . . 6 ⊢ (𝑓 = ∅ → (𝑓:∅⟶𝐵 ↔ ∅:∅⟶𝐵))
43	41, 42	bitr3id 194	. . . . 5 ⊢ (𝑓 = ∅ → ((𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓) ↔ ∅:∅⟶𝐵))
44	39, 43	spcev 2901	. . . 4 ⊢ (∅:∅⟶𝐵 → ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))
45	38, 44	mp1i 10	. . 3 ⊢ (∀𝑥 ∈ ∅ ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))
46		ssun1 3370	. . . . . . 7 ⊢ 𝑤 ⊆ (𝑤 ∪ {𝑧})
47		ssralv 3291	. . . . . . 7 ⊢ (𝑤 ⊆ (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑))
48	46, 47	ax-mp 5	. . . . . 6 ⊢ (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑)
49	48	imim1i 60	. . . . 5 ⊢ ((∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)))
50		ssun2 3371	. . . . . . . . 9 ⊢ {𝑧} ⊆ (𝑤 ∪ {𝑧})
51		ssralv 3291	. . . . . . . . 9 ⊢ ({𝑧} ⊆ (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ {𝑧}∃𝑦 ∈ 𝐵 𝜑))
52	50, 51	ax-mp 5	. . . . . . . 8 ⊢ (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ {𝑧}∃𝑦 ∈ 𝐵 𝜑)
53		vex 2805	. . . . . . . . . 10 ⊢ 𝑧 ∈ V
54		ralsnsg 3706	. . . . . . . . . 10 ⊢ (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}∃𝑦 ∈ 𝐵 𝜑 ↔ [𝑧 / 𝑥]∃𝑦 ∈ 𝐵 𝜑))
55	53, 54	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑥 ∈ {𝑧}∃𝑦 ∈ 𝐵 𝜑 ↔ [𝑧 / 𝑥]∃𝑦 ∈ 𝐵 𝜑)
56		sbcrex 3111	. . . . . . . . 9 ⊢ ([𝑧 / 𝑥]∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑)
57	55, 56	bitri 184	. . . . . . . 8 ⊢ (∀𝑥 ∈ {𝑧}∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑)
58	52, 57	sylib 122	. . . . . . 7 ⊢ (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑)
59		nfv 1576	. . . . . . . 8 ⊢ Ⅎ𝑦 ¬ 𝑧 ∈ 𝑤
60		nfv 1576	. . . . . . . . 9 ⊢ Ⅎ𝑦∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)
61		nfv 1576	. . . . . . . . . . 11 ⊢ Ⅎ𝑦 𝑔:(𝑤 ∪ {𝑧})⟶𝐵
62		nfcv 2374	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝑤 ∪ {𝑧})
63		nfsbc1v 3050	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦[(𝑔‘𝑥) / 𝑦]𝜑
64	62, 63	nfralxy 2570	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑
65	61, 64	nfan 1613	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)
66	65	nfex 1685	. . . . . . . . 9 ⊢ Ⅎ𝑦∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)
67	60, 66	nfim 1620	. . . . . . . 8 ⊢ Ⅎ𝑦(∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))
68		simprl 531	. . . . . . . . . . . . 13 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → 𝑓:𝑤⟶𝐵)
69		vex 2805	. . . . . . . . . . . . . . . 16 ⊢ 𝑦 ∈ V
70	53, 69	f1osn 5625	. . . . . . . . . . . . . . 15 ⊢ {⟨𝑧, 𝑦⟩}:{𝑧}–1-1-onto→{𝑦}
71		f1of 5583	. . . . . . . . . . . . . . 15 ⊢ ({⟨𝑧, 𝑦⟩}:{𝑧}–1-1-onto→{𝑦} → {⟨𝑧, 𝑦⟩}:{𝑧}⟶{𝑦})
72	70, 71	mp1i 10	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → {⟨𝑧, 𝑦⟩}:{𝑧}⟶{𝑦})
73		simpl2 1027	. . . . . . . . . . . . . . 15 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → 𝑦 ∈ 𝐵)
74	73	snssd 3818	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → {𝑦} ⊆ 𝐵)
75	72, 74	fssd 5495	. . . . . . . . . . . . 13 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → {⟨𝑧, 𝑦⟩}:{𝑧}⟶𝐵)
76		simpl1 1026	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ¬ 𝑧 ∈ 𝑤)
77		disjsn 3731	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑤)
78	76, 77	sylibr 134	. . . . . . . . . . . . 13 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (𝑤 ∩ {𝑧}) = ∅)
79		fun2 5509	. . . . . . . . . . . . 13 ⊢ (((𝑓:𝑤⟶𝐵 ∧ {⟨𝑧, 𝑦⟩}:{𝑧}⟶𝐵) ∧ (𝑤 ∩ {𝑧}) = ∅) → (𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵)
80	68, 75, 78, 79	syl21anc 1272	. . . . . . . . . . . 12 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵)
81		simprr 533	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ∀𝑥 ∈ 𝑤 𝜓)
82		eleq1a 2303	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝑤 → (𝑧 = 𝑥 → 𝑧 ∈ 𝑤))
83	82	necon3bd 2445	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝑤 → (¬ 𝑧 ∈ 𝑤 → 𝑧 ≠ 𝑥))
84	83	impcom 125	. . . . . . . . . . . . . . . . 17 ⊢ ((¬ 𝑧 ∈ 𝑤 ∧ 𝑥 ∈ 𝑤) → 𝑧 ≠ 𝑥)
85		fvunsng 5847	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ V ∧ 𝑧 ≠ 𝑥) → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = (𝑓‘𝑥))
86	20, 85	mpan 424	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ≠ 𝑥 → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = (𝑓‘𝑥))
87		dfsbcq 3033	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = (𝑓‘𝑥) → ([((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑 ↔ [(𝑓‘𝑥) / 𝑦]𝜑))
88	87, 23	bitr2di 197	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = (𝑓‘𝑥) → (𝜓 ↔ [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
89	84, 86, 88	3syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((¬ 𝑧 ∈ 𝑤 ∧ 𝑥 ∈ 𝑤) → (𝜓 ↔ [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
90	89	ralbidva 2528	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑧 ∈ 𝑤 → (∀𝑥 ∈ 𝑤 𝜓 ↔ ∀𝑥 ∈ 𝑤 [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
91	76, 90	syl 14	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (∀𝑥 ∈ 𝑤 𝜓 ↔ ∀𝑥 ∈ 𝑤 [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
92	81, 91	mpbid 147	. . . . . . . . . . . . 13 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ∀𝑥 ∈ 𝑤 [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)
93		simpl3 1028	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → [𝑧 / 𝑥]𝜑)
94		ffun 5485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵 → Fun (𝑓 ∪ {⟨𝑧, 𝑦⟩}))
95		ssun2 3371	. . . . . . . . . . . . . . . . . 18 ⊢ {⟨𝑧, 𝑦⟩} ⊆ (𝑓 ∪ {⟨𝑧, 𝑦⟩})
96		vsnid 3701	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑧 ∈ {𝑧}
97	69	dmsnop 5210	. . . . . . . . . . . . . . . . . . 19 ⊢ dom {⟨𝑧, 𝑦⟩} = {𝑧}
98	96, 97	eleqtrri 2307	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑧 ∈ dom {⟨𝑧, 𝑦⟩}
99		funssfv 5665	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun (𝑓 ∪ {⟨𝑧, 𝑦⟩}) ∧ {⟨𝑧, 𝑦⟩} ⊆ (𝑓 ∪ {⟨𝑧, 𝑦⟩}) ∧ 𝑧 ∈ dom {⟨𝑧, 𝑦⟩}) → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) = ({⟨𝑧, 𝑦⟩}‘𝑧))
100	95, 98, 99	mp3an23 1365	. . . . . . . . . . . . . . . . 17 ⊢ (Fun (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) = ({⟨𝑧, 𝑦⟩}‘𝑧))
101	80, 94, 100	3syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) = ({⟨𝑧, 𝑦⟩}‘𝑧))
102	53, 69	fvsn 5848	. . . . . . . . . . . . . . . 16 ⊢ ({⟨𝑧, 𝑦⟩}‘𝑧) = 𝑦
103	101, 102	eqtr2di 2281	. . . . . . . . . . . . . . 15 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → 𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧))
104		ralsnsg 3706	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}𝜑 ↔ [𝑧 / 𝑥]𝜑))
105	53, 104	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑥 ∈ {𝑧}𝜑 ↔ [𝑧 / 𝑥]𝜑)
106		elsni 3687	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ {𝑧} → 𝑥 = 𝑧)
107	106	fveq2d 5643	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ {𝑧} → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧))
108	107	eqeq2d 2243	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ {𝑧} → (𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) ↔ 𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧)))
109	108	biimparc 299	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) ∧ 𝑥 ∈ {𝑧}) → 𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥))
110		sbceq1a 3041	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) → (𝜑 ↔ [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
111	109, 110	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) ∧ 𝑥 ∈ {𝑧}) → (𝜑 ↔ [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
112	111	ralbidva 2528	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) → (∀𝑥 ∈ {𝑧}𝜑 ↔ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
113	105, 112	bitr3id 194	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) → ([𝑧 / 𝑥]𝜑 ↔ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
114	103, 113	syl 14	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ([𝑧 / 𝑥]𝜑 ↔ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
115	93, 114	mpbid 147	. . . . . . . . . . . . 13 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)
116		ralun 3389	. . . . . . . . . . . . 13 ⊢ ((∀𝑥 ∈ 𝑤 [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑 ∧ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑) → ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)
117	92, 115, 116	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)
118	53, 69	opex 4321	. . . . . . . . . . . . . . 15 ⊢ ⟨𝑧, 𝑦⟩ ∈ V
119	118	snex 4275	. . . . . . . . . . . . . 14 ⊢ {⟨𝑧, 𝑦⟩} ∈ V
120	19, 119	unex 4538	. . . . . . . . . . . . 13 ⊢ (𝑓 ∪ {⟨𝑧, 𝑦⟩}) ∈ V
121		feq1 5465	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → (𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ↔ (𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵))
122		fveq1 5638	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → (𝑔‘𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥))
123	122	sbceq1d 3036	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → ([(𝑔‘𝑥) / 𝑦]𝜑 ↔ [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
124	123	ralbidv 2532	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
125	121, 124	anbi12d 473	. . . . . . . . . . . . 13 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → ((𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑) ↔ ((𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)))
126	120, 125	spcev 2901	. . . . . . . . . . . 12 ⊢ (((𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))
127	80, 117, 126	syl2anc 411	. . . . . . . . . . 11 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))
128	127	ex 115	. . . . . . . . . 10 ⊢ ((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) → ((𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))
129	128	exlimdv 1867	. . . . . . . . 9 ⊢ ((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) → (∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))
130	129	3exp 1228	. . . . . . . 8 ⊢ (¬ 𝑧 ∈ 𝑤 → (𝑦 ∈ 𝐵 → ([𝑧 / 𝑥]𝜑 → (∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))))
131	59, 67, 130	rexlimd 2647	. . . . . . 7 ⊢ (¬ 𝑧 ∈ 𝑤 → (∃𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑 → (∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))))
132	58, 131	syl5 32	. . . . . 6 ⊢ (¬ 𝑧 ∈ 𝑤 → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → (∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))))
133	132	a2d 26	. . . . 5 ⊢ (¬ 𝑧 ∈ 𝑤 → ((∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))))
134	49, 133	syl5 32	. . . 4 ⊢ (¬ 𝑧 ∈ 𝑤 → ((∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))))
135	134	adantl 277	. . 3 ⊢ ((𝑤 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑤) → ((∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))))
136	6, 12, 31, 37, 45, 135	findcard2s 7078	. 2 ⊢ (𝐴 ∈ Fin → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓)))
137	136	imp 124	1 ⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 1004   = wceq 1397  ∃wex 1540   ∈ wcel 2202   ≠ wne 2402  ∀wral 2510  ∃wrex 2511  Vcvv 2802  [wsbc 3031   ∪ cun 3198   ∩ cin 3199   ⊆ wss 3200  ∅c0 3494  {csn 3669  ⟨cop 3672  dom cdm 4725  Fun wfun 5320  ⟶wf 5322  –1-1-onto→wf1o 5325  ‘cfv 5326  Fincfn 6908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-coll 4204  ax-sep 4207  ax-nul 4215  ax-pow 4264  ax-pr 4299  ax-un 4530  ax-setind 4635  ax-iinf 4686

This theorem depends on definitions:  df-bi 117  df-dc 842  df-3or 1005  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-ral 2515  df-rex 2516  df-reu 2517  df-rab 2519  df-v 2804  df-sbc 3032  df-csb 3128  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-nul 3495  df-if 3606  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-int 3929  df-iun 3972  df-br 4089  df-opab 4151  df-mpt 4152  df-tr 4188  df-id 4390  df-iord 4463  df-on 4465  df-suc 4468  df-iom 4689  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-rn 4736  df-res 4737  df-ima 4738  df-iota 5286  df-fun 5328  df-fn 5329  df-f 5330  df-f1 5331  df-fo 5332  df-f1o 5333  df-fv 5334  df-er 6701  df-en 6909  df-fin 6911

This theorem is referenced by:  finacn  7418