Theorem ac6sfi 9231

Description: A version of ac6s 10437 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 3296	. . . 4 ⊢ (𝑢 = ∅ → (∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ ∅ ∃𝑦 ∈ 𝐵 𝜑))
2		feq2 6667	. . . . . 6 ⊢ (𝑢 = ∅ → (𝑓:𝑢⟶𝐵 ↔ 𝑓:∅⟶𝐵))
3		raleq 3296	. . . . . 6 ⊢ (𝑢 = ∅ → (∀𝑥 ∈ 𝑢 𝜓 ↔ ∀𝑥 ∈ ∅ 𝜓))
4	2, 3	anbi12d 632	. . . . 5 ⊢ (𝑢 = ∅ → ((𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ (𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓)))
5	4	exbidv 1921	. . . 4 ⊢ (𝑢 = ∅ → (∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓)))
6	1, 5	imbi12d 344	. . 3 ⊢ (𝑢 = ∅ → ((∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓)) ↔ (∀𝑥 ∈ ∅ ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))))
7		raleq 3296	. . . 4 ⊢ (𝑢 = 𝑤 → (∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑))
8		feq2 6667	. . . . . 6 ⊢ (𝑢 = 𝑤 → (𝑓:𝑢⟶𝐵 ↔ 𝑓:𝑤⟶𝐵))
9		raleq 3296	. . . . . 6 ⊢ (𝑢 = 𝑤 → (∀𝑥 ∈ 𝑢 𝜓 ↔ ∀𝑥 ∈ 𝑤 𝜓))
10	8, 9	anbi12d 632	. . . . 5 ⊢ (𝑢 = 𝑤 → ((𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)))
11	10	exbidv 1921	. . . 4 ⊢ (𝑢 = 𝑤 → (∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)))
12	7, 11	imbi12d 344	. . 3 ⊢ (𝑢 = 𝑤 → ((∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓)) ↔ (∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓))))
13		raleq 3296	. . . 4 ⊢ (𝑢 = (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑))
14		feq2 6667	. . . . . . 7 ⊢ (𝑢 = (𝑤 ∪ {𝑧}) → (𝑓:𝑢⟶𝐵 ↔ 𝑓:(𝑤 ∪ {𝑧})⟶𝐵))
15		raleq 3296	. . . . . . 7 ⊢ (𝑢 = (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ 𝑢 𝜓 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓))
16	14, 15	anbi12d 632	. . . . . 6 ⊢ (𝑢 = (𝑤 ∪ {𝑧}) → ((𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ (𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓)))
17	16	exbidv 1921	. . . . 5 ⊢ (𝑢 = (𝑤 ∪ {𝑧}) → (∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ ∃𝑓(𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓)))
18		feq1 6666	. . . . . . 7 ⊢ (𝑓 = 𝑔 → (𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ↔ 𝑔:(𝑤 ∪ {𝑧})⟶𝐵))
19		fvex 6871	. . . . . . . . . 10 ⊢ (𝑓‘𝑥) ∈ V
20		ac6sfi.1	. . . . . . . . . 10 ⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓))
21	19, 20	sbcie 3795	. . . . . . . . 9 ⊢ ([(𝑓‘𝑥) / 𝑦]𝜑 ↔ 𝜓)
22		fveq1 6857	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑥) = (𝑔‘𝑥))
23	22	sbceq1d 3758	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → ([(𝑓‘𝑥) / 𝑦]𝜑 ↔ [(𝑔‘𝑥) / 𝑦]𝜑))
24	21, 23	bitr3id 285	. . . . . . . 8 ⊢ (𝑓 = 𝑔 → (𝜓 ↔ [(𝑔‘𝑥) / 𝑦]𝜑))
25	24	ralbidv 3156	. . . . . . 7 ⊢ (𝑓 = 𝑔 → (∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))
26	18, 25	anbi12d 632	. . . . . 6 ⊢ (𝑓 = 𝑔 → ((𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓) ↔ (𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))
27	26	cbvexvw 2037	. . . . 5 ⊢ (∃𝑓(𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓) ↔ ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))
28	17, 27	bitrdi 287	. . . 4 ⊢ (𝑢 = (𝑤 ∪ {𝑧}) → (∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))
29	13, 28	imbi12d 344	. . 3 ⊢ (𝑢 = (𝑤 ∪ {𝑧}) → ((∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓)) ↔ (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))))
30		raleq 3296	. . . 4 ⊢ (𝑢 = 𝐴 → (∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑))
31		feq2 6667	. . . . . 6 ⊢ (𝑢 = 𝐴 → (𝑓:𝑢⟶𝐵 ↔ 𝑓:𝐴⟶𝐵))
32		raleq 3296	. . . . . 6 ⊢ (𝑢 = 𝐴 → (∀𝑥 ∈ 𝑢 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜓))
33	31, 32	anbi12d 632	. . . . 5 ⊢ (𝑢 = 𝐴 → ((𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓)))
34	33	exbidv 1921	. . . 4 ⊢ (𝑢 = 𝐴 → (∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓)))
35	30, 34	imbi12d 344	. . 3 ⊢ (𝑢 = 𝐴 → ((∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓)) ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓))))
36		f0 6741	. . . 4 ⊢ ∅:∅⟶𝐵
37		0ex 5262	. . . . 5 ⊢ ∅ ∈ V
38		ral0 4476	. . . . . . 7 ⊢ ∀𝑥 ∈ ∅ 𝜓
39	38	biantru 529	. . . . . 6 ⊢ (𝑓:∅⟶𝐵 ↔ (𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))
40		feq1 6666	. . . . . 6 ⊢ (𝑓 = ∅ → (𝑓:∅⟶𝐵 ↔ ∅:∅⟶𝐵))
41	39, 40	bitr3id 285	. . . . 5 ⊢ (𝑓 = ∅ → ((𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓) ↔ ∅:∅⟶𝐵))
42	37, 41	spcev 3572	. . . 4 ⊢ (∅:∅⟶𝐵 → ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))
43	36, 42	mp1i 13	. . 3 ⊢ (∀𝑥 ∈ ∅ ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))
44		ssun1 4141	. . . . . . 7 ⊢ 𝑤 ⊆ (𝑤 ∪ {𝑧})
45		ssralv 4015	. . . . . . 7 ⊢ (𝑤 ⊆ (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑))
46	44, 45	ax-mp 5	. . . . . 6 ⊢ (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑)
47	46	imim1i 63	. . . . 5 ⊢ ((∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)))
48		ssun2 4142	. . . . . . . . 9 ⊢ {𝑧} ⊆ (𝑤 ∪ {𝑧})
49		ssralv 4015	. . . . . . . . 9 ⊢ ({𝑧} ⊆ (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ {𝑧}∃𝑦 ∈ 𝐵 𝜑))
50	48, 49	ax-mp 5	. . . . . . . 8 ⊢ (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ {𝑧}∃𝑦 ∈ 𝐵 𝜑)
51		ralsnsg 4634	. . . . . . . . . 10 ⊢ (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}∃𝑦 ∈ 𝐵 𝜑 ↔ [𝑧 / 𝑥]∃𝑦 ∈ 𝐵 𝜑))
52	51	elv 3452	. . . . . . . . 9 ⊢ (∀𝑥 ∈ {𝑧}∃𝑦 ∈ 𝐵 𝜑 ↔ [𝑧 / 𝑥]∃𝑦 ∈ 𝐵 𝜑)
53		sbcrex 3838	. . . . . . . . 9 ⊢ ([𝑧 / 𝑥]∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑)
54	52, 53	bitri 275	. . . . . . . 8 ⊢ (∀𝑥 ∈ {𝑧}∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑)
55	50, 54	sylib 218	. . . . . . 7 ⊢ (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑)
56		nfv 1914	. . . . . . . 8 ⊢ Ⅎ𝑦 ¬ 𝑧 ∈ 𝑤
57		nfv 1914	. . . . . . . . 9 ⊢ Ⅎ𝑦∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)
58		nfv 1914	. . . . . . . . . . 11 ⊢ Ⅎ𝑦 𝑔:(𝑤 ∪ {𝑧})⟶𝐵
59		nfcv 2891	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝑤 ∪ {𝑧})
60		nfsbc1v 3773	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦[(𝑔‘𝑥) / 𝑦]𝜑
61	59, 60	nfralw 3285	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑
62	58, 61	nfan 1899	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)
63	62	nfex 2323	. . . . . . . . 9 ⊢ Ⅎ𝑦∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)
64	57, 63	nfim 1896	. . . . . . . 8 ⊢ Ⅎ𝑦(∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))
65		simprl 770	. . . . . . . . . . . . 13 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → 𝑓:𝑤⟶𝐵)
66		vex 3451	. . . . . . . . . . . . . . . 16 ⊢ 𝑧 ∈ V
67		vex 3451	. . . . . . . . . . . . . . . 16 ⊢ 𝑦 ∈ V
68	66, 67	f1osn 6840	. . . . . . . . . . . . . . 15 ⊢ {⟨𝑧, 𝑦⟩}:{𝑧}–1-1-onto→{𝑦}
69		f1of 6800	. . . . . . . . . . . . . . 15 ⊢ ({⟨𝑧, 𝑦⟩}:{𝑧}–1-1-onto→{𝑦} → {⟨𝑧, 𝑦⟩}:{𝑧}⟶{𝑦})
70	68, 69	mp1i 13	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → {⟨𝑧, 𝑦⟩}:{𝑧}⟶{𝑦})
71		simpl2 1193	. . . . . . . . . . . . . . 15 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → 𝑦 ∈ 𝐵)
72	71	snssd 4773	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → {𝑦} ⊆ 𝐵)
73	70, 72	fssd 6705	. . . . . . . . . . . . 13 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → {⟨𝑧, 𝑦⟩}:{𝑧}⟶𝐵)
74		simpl1 1192	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ¬ 𝑧 ∈ 𝑤)
75		disjsn 4675	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑤)
76	74, 75	sylibr 234	. . . . . . . . . . . . 13 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (𝑤 ∩ {𝑧}) = ∅)
77	65, 73, 76	fun2d 6724	. . . . . . . . . . . 12 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵)
78		simprr 772	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ∀𝑥 ∈ 𝑤 𝜓)
79		eleq1a 2823	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝑤 → (𝑧 = 𝑥 → 𝑧 ∈ 𝑤))
80	79	necon3bd 2939	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝑤 → (¬ 𝑧 ∈ 𝑤 → 𝑧 ≠ 𝑥))
81	80	impcom 407	. . . . . . . . . . . . . . . . 17 ⊢ ((¬ 𝑧 ∈ 𝑤 ∧ 𝑥 ∈ 𝑤) → 𝑧 ≠ 𝑥)
82		fvunsn 7153	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ≠ 𝑥 → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = (𝑓‘𝑥))
83		dfsbcq 3755	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = (𝑓‘𝑥) → ([((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑 ↔ [(𝑓‘𝑥) / 𝑦]𝜑))
84	83, 21	bitr2di 288	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = (𝑓‘𝑥) → (𝜓 ↔ [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
85	81, 82, 84	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((¬ 𝑧 ∈ 𝑤 ∧ 𝑥 ∈ 𝑤) → (𝜓 ↔ [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
86	85	ralbidva 3154	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑧 ∈ 𝑤 → (∀𝑥 ∈ 𝑤 𝜓 ↔ ∀𝑥 ∈ 𝑤 [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
87	74, 86	syl 17	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (∀𝑥 ∈ 𝑤 𝜓 ↔ ∀𝑥 ∈ 𝑤 [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
88	78, 87	mpbid 232	. . . . . . . . . . . . 13 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ∀𝑥 ∈ 𝑤 [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)
89		simpl3 1194	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → [𝑧 / 𝑥]𝜑)
90		ffun 6691	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵 → Fun (𝑓 ∪ {⟨𝑧, 𝑦⟩}))
91		ssun2 4142	. . . . . . . . . . . . . . . . . 18 ⊢ {⟨𝑧, 𝑦⟩} ⊆ (𝑓 ∪ {⟨𝑧, 𝑦⟩})
92		vsnid 4627	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑧 ∈ {𝑧}
93	67	dmsnop 6189	. . . . . . . . . . . . . . . . . . 19 ⊢ dom {⟨𝑧, 𝑦⟩} = {𝑧}
94	92, 93	eleqtrri 2827	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑧 ∈ dom {⟨𝑧, 𝑦⟩}
95		funssfv 6879	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun (𝑓 ∪ {⟨𝑧, 𝑦⟩}) ∧ {⟨𝑧, 𝑦⟩} ⊆ (𝑓 ∪ {⟨𝑧, 𝑦⟩}) ∧ 𝑧 ∈ dom {⟨𝑧, 𝑦⟩}) → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) = ({⟨𝑧, 𝑦⟩}‘𝑧))
96	91, 94, 95	mp3an23 1455	. . . . . . . . . . . . . . . . 17 ⊢ (Fun (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) = ({⟨𝑧, 𝑦⟩}‘𝑧))
97	77, 90, 96	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) = ({⟨𝑧, 𝑦⟩}‘𝑧))
98	66, 67	fvsn 7155	. . . . . . . . . . . . . . . 16 ⊢ ({⟨𝑧, 𝑦⟩}‘𝑧) = 𝑦
99	97, 98	eqtr2di 2781	. . . . . . . . . . . . . . 15 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → 𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧))
100		ralsnsg 4634	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}𝜑 ↔ [𝑧 / 𝑥]𝜑))
101	100	elv 3452	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑥 ∈ {𝑧}𝜑 ↔ [𝑧 / 𝑥]𝜑)
102		elsni 4606	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ {𝑧} → 𝑥 = 𝑧)
103	102	fveq2d 6862	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ {𝑧} → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧))
104	103	eqeq2d 2740	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ {𝑧} → (𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) ↔ 𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧)))
105	104	biimparc 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) ∧ 𝑥 ∈ {𝑧}) → 𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥))
106		sbceq1a 3764	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) → (𝜑 ↔ [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
107	105, 106	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) ∧ 𝑥 ∈ {𝑧}) → (𝜑 ↔ [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
108	107	ralbidva 3154	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) → (∀𝑥 ∈ {𝑧}𝜑 ↔ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
109	101, 108	bitr3id 285	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) → ([𝑧 / 𝑥]𝜑 ↔ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
110	99, 109	syl 17	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ([𝑧 / 𝑥]𝜑 ↔ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
111	89, 110	mpbid 232	. . . . . . . . . . . . 13 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)
112		ralun 4161	. . . . . . . . . . . . 13 ⊢ ((∀𝑥 ∈ 𝑤 [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑 ∧ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑) → ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)
113	88, 111, 112	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)
114		vex 3451	. . . . . . . . . . . . . 14 ⊢ 𝑓 ∈ V
115		snex 5391	. . . . . . . . . . . . . 14 ⊢ {⟨𝑧, 𝑦⟩} ∈ V
116	114, 115	unex 7720	. . . . . . . . . . . . 13 ⊢ (𝑓 ∪ {⟨𝑧, 𝑦⟩}) ∈ V
117		feq1 6666	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → (𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ↔ (𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵))
118		fveq1 6857	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → (𝑔‘𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥))
119	118	sbceq1d 3758	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → ([(𝑔‘𝑥) / 𝑦]𝜑 ↔ [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
120	119	ralbidv 3156	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
121	117, 120	anbi12d 632	. . . . . . . . . . . . 13 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → ((𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑) ↔ ((𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)))
122	116, 121	spcev 3572	. . . . . . . . . . . 12 ⊢ (((𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))
123	77, 113, 122	syl2anc 584	. . . . . . . . . . 11 ⊢ (((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))
124	123	ex 412	. . . . . . . . . 10 ⊢ ((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) → ((𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))
125	124	exlimdv 1933	. . . . . . . . 9 ⊢ ((¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) → (∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))
126	125	3exp 1119	. . . . . . . 8 ⊢ (¬ 𝑧 ∈ 𝑤 → (𝑦 ∈ 𝐵 → ([𝑧 / 𝑥]𝜑 → (∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))))
127	56, 64, 126	rexlimd 3244	. . . . . . 7 ⊢ (¬ 𝑧 ∈ 𝑤 → (∃𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑 → (∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))))
128	55, 127	syl5 34	. . . . . 6 ⊢ (¬ 𝑧 ∈ 𝑤 → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → (∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))))
129	128	a2d 29	. . . . 5 ⊢ (¬ 𝑧 ∈ 𝑤 → ((∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))))
130	47, 129	syl5 34	. . . 4 ⊢ (¬ 𝑧 ∈ 𝑤 → ((∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))))
131	130	adantl 481	. . 3 ⊢ ((𝑤 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑤) → ((∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))))
132	6, 12, 29, 35, 43, 131	findcard2s 9129	. 2 ⊢ (𝐴 ∈ Fin → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓)))
133	132	imp 406	1 ⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  ∃wrex 3053  Vcvv 3447  [wsbc 3753   ∪ cun 3912   ∩ cin 3913   ⊆ wss 3914  ∅c0 4296  {csn 4589  ⟨cop 4595  dom cdm 5638  Fun wfun 6505  ⟶wf 6507  –1-1-onto→wf1o 6510  ‘cfv 6511  Fincfn 8918

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-om 7843  df-en 8919  df-fin 8922

This theorem is referenced by:  fissuni  9308  fipreima  9309  indexfi  9311  finacn  10003  axcc4dom  10394  ttukeylem6  10467  firest  17395  ablfaclem3  20019  ablfac2  20021  cmpcovf  23278  cmpsub  23287  tgcmp  23288  hauscmplem  23293  comppfsc  23419  ptcnplem  23508  alexsubALTlem3  23936  alexsubALT  23938  tsmsxplem1  24040  ovolicc2lem5  25422  ovolicc2  25423  limciun  25795  cvmliftlem15  35285  matunitlindflem2  37611  ptrecube  37614  istotbnd3  37765  sstotbnd2  37768  sstotbnd  37769  prdsbnd  37787  prdstotbnd  37788  heiborlem1  37805  heibor  37815  kelac1  43052  hbt  43119