Theorem ac6sfi 9240

Description: A version of ac6s 10472 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 3320	. . . 4 ⊢ (𝑢 = ∅ → (∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ ∅ ∃𝑦 ∈ 𝐵 𝜑))
2		feq2 6684	. . . . . 6 ⊢ (𝑢 = ∅ → (𝑓:𝑢⟶𝐵 ↔ 𝑓:∅⟶𝐵))
3		raleq 3320	. . . . . 6 ⊢ (𝑢 = ∅ → (∀𝑥 ∈ 𝑢 𝜓 ↔ ∀𝑥 ∈ ∅ 𝜓))
4	2, 3	anbi12d 643	. . . . 5 ⊢ (𝑢 = ∅ → ((𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ (𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓)))
5	4	exbidv 1951	. . . 4 ⊢ (𝑢 = ∅ → (∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓)))
6	1, 5	imbi12d 347	. . 3 ⊢ (𝑢 = ∅ → ((∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓)) ↔ (∀𝑥 ∈ ∅ ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))))
7		raleq 3320	. . . 4 ⊢ (𝑢 = 𝑤 → (∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑))
8		feq2 6684	. . . . . 6 ⊢ (𝑢 = 𝑤 → (𝑓:𝑢⟶𝐵 ↔ 𝑓:𝑤⟶𝐵))
9		raleq 3320	. . . . . 6 ⊢ (𝑢 = 𝑤 → (∀𝑥 ∈ 𝑢 𝜓 ↔ ∀𝑥 ∈ 𝑤 𝜓))
10	8, 9	anbi12d 643	. . . . 5 ⊢ (𝑢 = 𝑤 → ((𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)))
11	10	exbidv 1951	. . . 4 ⊢ (𝑢 = 𝑤 → (∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)))
12	7, 11	imbi12d 347	. . 3 ⊢ (𝑢 = 𝑤 → ((∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓)) ↔ (∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓))))
13		raleq 3320	. . . 4 ⊢ (𝑢 = (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑))
14		feq2 6684	. . . . . . 7 ⊢ (𝑢 = (𝑤 ∪ {𝑧}) → (𝑓:𝑢⟶𝐵 ↔ 𝑓:(𝑤 ∪ {𝑧})⟶𝐵))
15		raleq 3320	. . . . . . 7 ⊢ (𝑢 = (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ 𝑢 𝜓 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓))
16	14, 15	anbi12d 643	. . . . . 6 ⊢ (𝑢 = (𝑤 ∪ {𝑧}) → ((𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ (𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓)))
17	16	exbidv 1951	. . . . 5 ⊢ (𝑢 = (𝑤 ∪ {𝑧}) → (∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ ∃𝑓(𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓)))
18		feq1 6683	. . . . . . 7 ⊢ (𝑓 = 𝑔 → (𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ↔ 𝑔:(𝑤 ∪ {𝑧})⟶𝐵))
19		fvex 6894	. . . . . . . . . 10 ⊢ (𝑓‘𝑥) ∈ V
20		ac6sfi.1	. . . . . . . . . 10 ⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓))
21	19, 20	sbcie 3785	. . . . . . . . 9 ⊢ ([(𝑓‘𝑥) / 𝑦]𝜑 ↔ 𝜓)
22		fveq1 6880	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑥) = (𝑔‘𝑥))
23	22	sbceq1d 3749	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → ([(𝑓‘𝑥) / 𝑦]𝜑 ↔ [(𝑔‘𝑥) / 𝑦]𝜑))
24	21, 23	bitr3id 288	. . . . . . . 8 ⊢ (𝑓 = 𝑔 → (𝜓 ↔ [(𝑔‘𝑥) / 𝑦]𝜑))
25	24	ralbidv 3188	. . . . . . 7 ⊢ (𝑓 = 𝑔 → (∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))
26	18, 25	anbi12d 643	. . . . . 6 ⊢ (𝑓 = 𝑔 → ((𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓) ↔ (𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))
27	26	cbvexvw 2067	. . . . 5 ⊢ (∃𝑓(𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓) ↔ ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))
28	17, 27	bitrdi 290	. . . 4 ⊢ (𝑢 = (𝑤 ∪ {𝑧}) → (∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))
29	13, 28	imbi12d 347	. . 3 ⊢ (𝑢 = (𝑤 ∪ {𝑧}) → ((∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓)) ↔ (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))))
30		raleq 3320	. . . 4 ⊢ (𝑢 = 𝐴 → (∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑))
31		feq2 6684	. . . . . 6 ⊢ (𝑢 = 𝐴 → (𝑓:𝑢⟶𝐵 ↔ 𝑓:𝐴⟶𝐵))
32		raleq 3320	. . . . . 6 ⊢ (𝑢 = 𝐴 → (∀𝑥 ∈ 𝑢 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜓))
33	31, 32	anbi12d 643	. . . . 5 ⊢ (𝑢 = 𝐴 → ((𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓)))
34	33	exbidv 1951	. . . 4 ⊢ (𝑢 = 𝐴 → (∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓)))
35	30, 34	imbi12d 347	. . 3 ⊢ (𝑢 = 𝐴 → ((∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓)) ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓))))
36		f0 6759	. . . 4 ⊢ ∅:∅⟶𝐵
37		0ex 5270	. . . . 5 ⊢ ∅ ∈ V
38		ral0 4459	. . . . . . 7 ⊢ ∀𝑥 ∈ ∅ 𝜓
39	38	biantru 538	. . . . . 6 ⊢ (𝑓:∅⟶𝐵 ↔ (𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))
40		feq1 6683	. . . . . 6 ⊢ (𝑓 = ∅ → (𝑓:∅⟶𝐵 ↔ ∅:∅⟶𝐵))
41	39, 40	bitr3id 288	. . . . 5 ⊢ (𝑓 = ∅ → ((𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓) ↔ ∅:∅⟶𝐵))
42	37, 41	spcev 3565	. . . 4 ⊢ (∅:∅⟶𝐵 → ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))
43	36, 42	mp1i 14	. . 3 ⊢ (∀𝑥 ∈ ∅ ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))
44		ssun1 4131	. . . . . . 7 ⊢ 𝑤 ⊆ (𝑤 ∪ {𝑧})
45		ssralv 4006	. . . . . . 7 ⊢ (𝑤 ⊆ (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑))
46	44, 45	ax-mp 5	. . . . . 6 ⊢ (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑)
47	46	imim1i 64	. . . . 5 ⊢ ((∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)))
48		ssun2 4132	. . . . . . . . 9 ⊢ {𝑧} ⊆ (𝑤 ∪ {𝑧})
49		ssralv 4006	. . . . . . . . 9 ⊢ ({𝑧} ⊆ (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ {𝑧}∃𝑦 ∈ 𝐵 𝜑))
50	48, 49	ax-mp 5	. . . . . . . 8 ⊢ (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ {𝑧}∃𝑦 ∈ 𝐵 𝜑)
51		ralsnsg 4636	. . . . . . . . . 10 ⊢ (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}∃𝑦 ∈ 𝐵 𝜑 ↔ [𝑧 / 𝑥]∃𝑦 ∈ 𝐵 𝜑))
52	51	elv 3460	. . . . . . . . 9 ⊢ (∀𝑥 ∈ {𝑧}∃𝑦 ∈ 𝐵 𝜑 ↔ [𝑧 / 𝑥]∃𝑦 ∈ 𝐵 𝜑)
53		sbcrex 3828	. . . . . . . . 9 ⊢ ([𝑧 / 𝑥]∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑)
54	52, 53	bitri 278	. . . . . . . 8 ⊢ (∀𝑥 ∈ {𝑧}∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑)
55	50, 54	sylib 221	. . . . . . 7 ⊢ (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑)
56		nfv 1944	. . . . . . . 8 ⊢ Ⅎ𝑦 ¬ 𝑧 ∈ 𝑤
57		nfv 1944	. . . . . . . . 9 ⊢ Ⅎ𝑦∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)
58		nfv 1944	. . . . . . . . . . 11 ⊢ Ⅎ𝑦 𝑔:(𝑤 ∪ {𝑧})⟶𝐵
59		nfcv 2925	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝑤 ∪ {𝑧})
60		nfsbc1v 3764	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦[(𝑔‘𝑥) / 𝑦]𝜑
61	59, 60	nfralw 3312	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑
62	58, 61	nfan 1929	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)
63	62	nfex 2357	. . . . . . . . 9 ⊢ Ⅎ𝑦∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)
64	57, 63	nfim 1926	. . . . . . . 8 ⊢ Ⅎ𝑦(∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))
65		simprl 782	. . . . . . . . . . . . 13 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → 𝑓:𝑤⟶𝐵)
66		vex 3459	. . . . . . . . . . . . . . . 16 ⊢ 𝑧 ∈ V
67		vex 3459	. . . . . . . . . . . . . . . 16 ⊢ 𝑦 ∈ V
68	66, 67	f1osn 6862	. . . . . . . . . . . . . . 15 ⊢ {⟨𝑧, 𝑦⟩}:{𝑧}–1-1-onto→{𝑦}
69		f1of 6820	. . . . . . . . . . . . . . 15 ⊢ ({⟨𝑧, 𝑦⟩}:{𝑧}–1-1-onto→{𝑦} → {⟨𝑧, 𝑦⟩}:{𝑧}⟶{𝑦})
70	68, 69	mp1i 14	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → {⟨𝑧, 𝑦⟩}:{𝑧}⟶{𝑦})
71		simpl2 1211	. . . . . . . . . . . . . . 15 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → 𝑦 ∈ 𝐵)
72	71	snssd 4752	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → {𝑦} ⊆ 𝐵)
73	70, 72	fssd 6723	. . . . . . . . . . . . 13 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → {⟨𝑧, 𝑦⟩}:{𝑧}⟶𝐵)
74		simpl1 1210	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ¬ 𝑧 ∈ 𝑤)
75		disjsn 4677	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑤)
76	74, 75	sylibr 237	. . . . . . . . . . . . 13 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (𝑤 ∩ {𝑧}) = ∅)
77	65, 73, 76	fun2d 6742	. . . . . . . . . . . 12 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵)
78		simprr 784	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ∀𝑥 ∈ 𝑤 𝜓)
79		eleq1a 2858	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝑤 → (𝑧 = 𝑥 → 𝑧 ∈ 𝑤))
80	79	necon3bd 2972	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝑤 → (¬ 𝑧 ∈ 𝑤 → 𝑧 ≠ 𝑥))
81	80	impcom 412	. . . . . . . . . . . . . . . . 17 ⊢ ((¬ 𝑧 ∈ 𝑤 ∧ 𝑥 ∈ 𝑤) → 𝑧 ≠ 𝑥)
82		fvunsn 7177	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ≠ 𝑥 → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = (𝑓‘𝑥))
83		dfsbcq 3746	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = (𝑓‘𝑥) → ([((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑 ↔ [(𝑓‘𝑥) / 𝑦]𝜑))
84	83, 21	bitr2di 291	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = (𝑓‘𝑥) → (𝜓 ↔ [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
85	81, 82, 84	3syl 19	. . . . . . . . . . . . . . . 16 ⊢ ((¬ 𝑧 ∈ 𝑤 ∧ 𝑥 ∈ 𝑤) → (𝜓 ↔ [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
86	85	ralbidva 3186	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑧 ∈ 𝑤 → (∀𝑥 ∈ 𝑤 𝜓 ↔ ∀𝑥 ∈ 𝑤 [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
87	74, 86	syl 18	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (∀𝑥 ∈ 𝑤 𝜓 ↔ ∀𝑥 ∈ 𝑤 [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
88	78, 87	mpbid 235	. . . . . . . . . . . . 13 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ∀𝑥 ∈ 𝑤 [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)
89		simpl3 1212	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → [𝑧 / 𝑥]𝜑)
90		ffun 6708	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵 → Fun (𝑓 ∪ {⟨𝑧, 𝑦⟩}))
91		ssun2 4132	. . . . . . . . . . . . . . . . . 18 ⊢ {⟨𝑧, 𝑦⟩} ⊆ (𝑓 ∪ {⟨𝑧, 𝑦⟩})
92		vsnid 4629	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑧 ∈ {𝑧}
93	67	dmsnop 6217	. . . . . . . . . . . . . . . . . . 19 ⊢ dom {⟨𝑧, 𝑦⟩} = {𝑧}
94	92, 93	eleqtrri 2862	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑧 ∈ dom {⟨𝑧, 𝑦⟩}
95		funssfv 6902	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun (𝑓 ∪ {⟨𝑧, 𝑦⟩}) ∧ {⟨𝑧, 𝑦⟩} ⊆ (𝑓 ∪ {⟨𝑧, 𝑦⟩}) ∧ 𝑧 ∈ dom {⟨𝑧, 𝑦⟩}) → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) = ({⟨𝑧, 𝑦⟩}‘𝑧))
96	91, 94, 95	mp3an23 1482	. . . . . . . . . . . . . . . . 17 ⊢ (Fun (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) = ({⟨𝑧, 𝑦⟩}‘𝑧))
97	77, 90, 96	3syl 19	. . . . . . . . . . . . . . . 16 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) = ({⟨𝑧, 𝑦⟩}‘𝑧))
98	66, 67	fvsn 7179	. . . . . . . . . . . . . . . 16 ⊢ ({⟨𝑧, 𝑦⟩}‘𝑧) = 𝑦
99	97, 98	eqtr2di 2815	. . . . . . . . . . . . . . 15 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → 𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧))
100		ralsnsg 4636	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}𝜑 ↔ [𝑧 / 𝑥]𝜑))
101	100	elv 3460	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑥 ∈ {𝑧}𝜑 ↔ [𝑧 / 𝑥]𝜑)
102		elsni 4606	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ {𝑧} → 𝑥 = 𝑧)
103	102	fveq2d 6885	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ {𝑧} → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧))
104	103	eqeq2d 2774	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ {𝑧} → (𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) ↔ 𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧)))
105	104	biimparc 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) ∧ 𝑥 ∈ {𝑧}) → 𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥))
106		sbceq1a 3755	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) → (𝜑 ↔ [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
107	105, 106	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) ∧ 𝑥 ∈ {𝑧}) → (𝜑 ↔ [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
108	107	ralbidva 3186	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) → (∀𝑥 ∈ {𝑧}𝜑 ↔ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
109	101, 108	bitr3id 288	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) → ([𝑧 / 𝑥]𝜑 ↔ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
110	99, 109	syl 18	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ([𝑧 / 𝑥]𝜑 ↔ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
111	89, 110	mpbid 235	. . . . . . . . . . . . 13 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)
112		ralun 4151	. . . . . . . . . . . . 13 ⊢ ((∀𝑥 ∈ 𝑤 [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑 ∧ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑) → ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)
113	88, 111, 112	syl2anc 595	. . . . . . . . . . . 12 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)
114		vex 3459	. . . . . . . . . . . . . 14 ⊢ 𝑓 ∈ V
115		snex 5410	. . . . . . . . . . . . . 14 ⊢ {⟨𝑧, 𝑦⟩} ∈ V
116	114, 115	unex 7742	. . . . . . . . . . . . 13 ⊢ (𝑓 ∪ {⟨𝑧, 𝑦⟩}) ∈ V
117		feq1 6683	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → (𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ↔ (𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵))
118		fveq1 6880	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → (𝑔‘𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥))
119	118	sbceq1d 3749	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → ([(𝑔‘𝑥) / 𝑦]𝜑 ↔ [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
120	119	ralbidv 3188	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
121	117, 120	anbi12d 643	. . . . . . . . . . . . 13 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → ((𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑) ↔ ((𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)))
122	116, 121	spcev 3565	. . . . . . . . . . . 12 ⊢ (((𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))
123	77, 113, 122	syl2anc 595	. . . . . . . . . . 11 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))
124	123	ex 417	. . . . . . . . . 10 ⊢ ((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) → ((𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))
125	124	exlimdv 1963	. . . . . . . . 9 ⊢ ((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) → (∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))
126	125	3exp 1137	. . . . . . . 8 ⊢ (¬ 𝑧 ∈ 𝑤 → (𝑦 ∈ 𝐵 → ([𝑧 / 𝑥]𝜑 → (∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))))
127	56, 64, 126	rexlimd 3272	. . . . . . 7 ⊢ (¬ 𝑧 ∈ 𝑤 → (∃𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑 → (∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))))
128	55, 127	syl5 35	. . . . . 6 ⊢ (¬ 𝑧 ∈ 𝑤 → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → (∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))))
129	128	a2d 30	. . . . 5 ⊢ (¬ 𝑧 ∈ 𝑤 → ((∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))))
130	47, 129	syl5 35	. . . 4 ⊢ (¬ 𝑧 ∈ 𝑤 → ((∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))))
131	130	adantl 486	. . 3 ⊢ ((𝑤 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑤) → ((∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))))
132	6, 12, 29, 35, 43, 131	findcard2s 9146	. 2 ⊢ (𝐴 ∈ Fin → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓)))
133	132	imp 411	1 ⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1103   = wceq 1570  ∃wex 1809   ∈ wcel 2143   ≠ wne 2958  ∀wral 3079  ∃wrex 3089  Vcvv 3455  [wsbc 3744   ∪ cun 3903   ∩ cin 3904   ⊆ wss 3905  ∅c0 4286  {csn 4589  ⟨cop 4595  dom cdm 5661  Fun wfun 6530  ⟶wf 6532  –1-1-onto→wf1o 6535  ‘cfv 6536  Fincfn 8939

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404  ax-un 7732

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-om 7859  df-en 8940  df-fin 8943

This theorem is used by:  fissuni  9310  fipreima  9311  indexfi  9313  finacn  10039  axcc4dom  10429  ttukeylem6  10502  firest  17489  ablfaclem3  20163  ablfac2  20165  cmpcovf  23557  cmpsub  23566  tgcmp  23567  hauscmplem  23572  comppfsc  23698  ptcnplem  23787  alexsubALTlem3  24215  alexsubALT  24217  tsmsxplem1  24319  ovolicc2lem5  25689  ovolicc2  25690  limciun  26062  cvmliftlem15  35798  matunitlindflem2  38296  ptrecube  38299  istotbnd3  38450  sstotbnd2  38453  sstotbnd  38454  prdsbnd  38472  prdstotbnd  38473  heiborlem1  38490  heibor  38500  kelac1  43818  hbt  43885