Theorem fprod2dlem 15328

Description: Lemma for fprod2d 15329- induction step. (Contributed by Scott Fenton, 30-Jan-2018.)

Hypotheses

Ref	Expression
fprod2d.1	⊢ (𝑧 = ⟨𝑗, 𝑘⟩ → 𝐷 = 𝐶)
fprod2d.2	⊢ (𝜑 → 𝐴 ∈ Fin)
fprod2d.3	⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ Fin)
fprod2d.4	⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ ℂ)
fprod2d.5	⊢ (𝜑 → ¬ 𝑦 ∈ 𝑥)
fprod2d.6	⊢ (𝜑 → (𝑥 ∪ {𝑦}) ⊆ 𝐴)
fprod2d.7	⊢ (𝜓 ↔ ∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷)

Assertion

Ref	Expression
fprod2dlem	⊢ ((𝜑 ∧ 𝜓) → ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷)

Distinct variable groups:   𝐴,𝑗,𝑘   𝐵,𝑘,𝑧   𝑧,𝐶   𝐷,𝑗,𝑘   𝜑,𝑗   𝑥,𝑗   𝑦,𝑗,𝑧   𝜑,𝑘   𝑥,𝑘   𝑦,𝑘,𝑧   𝜑,𝑧   𝑥,𝑧   𝑦,𝑧

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦,𝑧,𝑗,𝑘)   𝐴(𝑥,𝑦,𝑧)   𝐵(𝑥,𝑦,𝑗)   𝐶(𝑥,𝑦,𝑗,𝑘)   𝐷(𝑥,𝑦,𝑧)

Proof of Theorem fprod2dlem

Dummy variable 𝑚 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 487	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2		fprod2d.7	. . . 4 ⊢ (𝜓 ↔ ∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷)
3	1, 2	sylib 220	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷)
4		nfcv 2977	. . . . . 6 ⊢ Ⅎ𝑚∏𝑘 ∈ 𝐵 𝐶
5		nfcsb1v 3906	. . . . . . 7 ⊢ Ⅎ𝑗⦋𝑚 / 𝑗⦌𝐵
6		nfcsb1v 3906	. . . . . . 7 ⊢ Ⅎ𝑗⦋𝑚 / 𝑗⦌𝐶
7	5, 6	nfcprod 15259	. . . . . 6 ⊢ Ⅎ𝑗∏𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐶
8		csbeq1a 3896	. . . . . . 7 ⊢ (𝑗 = 𝑚 → 𝐵 = ⦋𝑚 / 𝑗⦌𝐵)
9		csbeq1a 3896	. . . . . . . 8 ⊢ (𝑗 = 𝑚 → 𝐶 = ⦋𝑚 / 𝑗⦌𝐶)
10	9	adantr 483	. . . . . . 7 ⊢ ((𝑗 = 𝑚 ∧ 𝑘 ∈ 𝐵) → 𝐶 = ⦋𝑚 / 𝑗⦌𝐶)
11	8, 10	prodeq12dv 15274	. . . . . 6 ⊢ (𝑗 = 𝑚 → ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐶)
12	4, 7, 11	cbvprodi 15265	. . . . 5 ⊢ ∏𝑗 ∈ {𝑦}∏𝑘 ∈ 𝐵 𝐶 = ∏𝑚 ∈ {𝑦}∏𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐶
13		fprod2d.6	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∪ {𝑦}) ⊆ 𝐴)
14	13	unssbd 4163	. . . . . . . 8 ⊢ (𝜑 → {𝑦} ⊆ 𝐴)
15		vex 3497	. . . . . . . . 9 ⊢ 𝑦 ∈ V
16	15	snss 4711	. . . . . . . 8 ⊢ (𝑦 ∈ 𝐴 ↔ {𝑦} ⊆ 𝐴)
17	14, 16	sylibr 236	. . . . . . 7 ⊢ (𝜑 → 𝑦 ∈ 𝐴)
18		fprod2d.3	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ Fin)
19	18	ralrimiva 3182	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑗 ∈ 𝐴 𝐵 ∈ Fin)
20		nfcsb1v 3906	. . . . . . . . . . 11 ⊢ Ⅎ𝑗⦋𝑦 / 𝑗⦌𝐵
21	20	nfel1 2994	. . . . . . . . . 10 ⊢ Ⅎ𝑗⦋𝑦 / 𝑗⦌𝐵 ∈ Fin
22		csbeq1a 3896	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑗⦌𝐵)
23	22	eleq1d 2897	. . . . . . . . . 10 ⊢ (𝑗 = 𝑦 → (𝐵 ∈ Fin ↔ ⦋𝑦 / 𝑗⦌𝐵 ∈ Fin))
24	21, 23	rspc 3610	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝐴 → (∀𝑗 ∈ 𝐴 𝐵 ∈ Fin → ⦋𝑦 / 𝑗⦌𝐵 ∈ Fin))
25	17, 19, 24	sylc 65	. . . . . . . 8 ⊢ (𝜑 → ⦋𝑦 / 𝑗⦌𝐵 ∈ Fin)
26		fprod2d.4	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ ℂ)
27	26	ralrimivva 3191	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑗 ∈ 𝐴 ∀𝑘 ∈ 𝐵 𝐶 ∈ ℂ)
28		nfcsb1v 3906	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗⦋𝑦 / 𝑗⦌𝐶
29	28	nfel1 2994	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ
30	20, 29	nfralw 3225	. . . . . . . . . . 11 ⊢ Ⅎ𝑗∀𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ
31		csbeq1a 3896	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑗⦌𝐶)
32	31	eleq1d 2897	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑦 → (𝐶 ∈ ℂ ↔ ⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ))
33	22, 32	raleqbidv 3401	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑦 → (∀𝑘 ∈ 𝐵 𝐶 ∈ ℂ ↔ ∀𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ))
34	30, 33	rspc 3610	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝐴 → (∀𝑗 ∈ 𝐴 ∀𝑘 ∈ 𝐵 𝐶 ∈ ℂ → ∀𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ))
35	17, 27, 34	sylc 65	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ)
36	35	r19.21bi 3208	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵) → ⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ)
37	25, 36	fprodcl 15300	. . . . . . 7 ⊢ (𝜑 → ∏𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ)
38		csbeq1 3885	. . . . . . . . 9 ⊢ (𝑚 = 𝑦 → ⦋𝑚 / 𝑗⦌𝐵 = ⦋𝑦 / 𝑗⦌𝐵)
39		csbeq1 3885	. . . . . . . . . 10 ⊢ (𝑚 = 𝑦 → ⦋𝑚 / 𝑗⦌𝐶 = ⦋𝑦 / 𝑗⦌𝐶)
40	39	adantr 483	. . . . . . . . 9 ⊢ ((𝑚 = 𝑦 ∧ 𝑘 ∈ ⦋𝑚 / 𝑗⦌𝐵) → ⦋𝑚 / 𝑗⦌𝐶 = ⦋𝑦 / 𝑗⦌𝐶)
41	38, 40	prodeq12dv 15274	. . . . . . . 8 ⊢ (𝑚 = 𝑦 → ∏𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐶 = ∏𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶)
42	41	prodsn 15310	. . . . . . 7 ⊢ ((𝑦 ∈ 𝐴 ∧ ∏𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ) → ∏𝑚 ∈ {𝑦}∏𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐶 = ∏𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶)
43	17, 37, 42	syl2anc 586	. . . . . 6 ⊢ (𝜑 → ∏𝑚 ∈ {𝑦}∏𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐶 = ∏𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶)
44		nfcv 2977	. . . . . . . 8 ⊢ Ⅎ𝑚⦋𝑦 / 𝑗⦌𝐶
45		nfcsb1v 3906	. . . . . . . 8 ⊢ Ⅎ𝑘⦋𝑚 / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶
46		csbeq1a 3896	. . . . . . . 8 ⊢ (𝑘 = 𝑚 → ⦋𝑦 / 𝑗⦌𝐶 = ⦋𝑚 / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶)
47	44, 45, 46	cbvprodi 15265	. . . . . . 7 ⊢ ∏𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶 = ∏𝑚 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑚 / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶
48		csbeq1 3885	. . . . . . . . 9 ⊢ (𝑚 = (2nd ‘𝑧) → ⦋𝑚 / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶)
49		snfi 8588	. . . . . . . . . 10 ⊢ {𝑦} ∈ Fin
50		xpfi 8783	. . . . . . . . . 10 ⊢ (({𝑦} ∈ Fin ∧ ⦋𝑦 / 𝑗⦌𝐵 ∈ Fin) → ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵) ∈ Fin)
51	49, 25, 50	sylancr 589	. . . . . . . . 9 ⊢ (𝜑 → ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵) ∈ Fin)
52		2ndconst 7790	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝐴 → (2nd ↾ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)):({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)–1-1-onto→⦋𝑦 / 𝑗⦌𝐵)
53	17, 52	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (2nd ↾ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)):({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)–1-1-onto→⦋𝑦 / 𝑗⦌𝐵)
54		fvres 6683	. . . . . . . . . 10 ⊢ (𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵) → ((2nd ↾ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵))‘𝑧) = (2nd ‘𝑧))
55	54	adantl 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)) → ((2nd ↾ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵))‘𝑧) = (2nd ‘𝑧))
56	45	nfel1 2994	. . . . . . . . . . 11 ⊢ Ⅎ𝑘⦋𝑚 / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ
57	46	eleq1d 2897	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑚 → (⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ ↔ ⦋𝑚 / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ))
58	56, 57	rspc 3610	. . . . . . . . . 10 ⊢ (𝑚 ∈ ⦋𝑦 / 𝑗⦌𝐵 → (∀𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ → ⦋𝑚 / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ))
59	35, 58	mpan9 509	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ⦋𝑦 / 𝑗⦌𝐵) → ⦋𝑚 / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ)
60	48, 51, 53, 55, 59	fprodf1o 15294	. . . . . . . 8 ⊢ (𝜑 → ∏𝑚 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑚 / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶 = ∏𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶)
61		elxp 5572	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵) ↔ ∃𝑚∃𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵)))
62		nfv 1911	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑗 𝑧 = ⟨𝑚, 𝑘⟩
63		nfv 1911	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑗 𝑚 ∈ {𝑦}
64	20	nfcri 2971	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑗 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵
65	63, 64	nfan 1896	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑗(𝑚 ∈ {𝑦} ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵)
66	62, 65	nfan 1896	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵))
67	66	nfex 2339	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗∃𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵))
68		nfv 1911	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑚∃𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵))
69		opeq1 4796	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑗 → ⟨𝑚, 𝑘⟩ = ⟨𝑗, 𝑘⟩)
70	69	eqeq2d 2832	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑗 → (𝑧 = ⟨𝑚, 𝑘⟩ ↔ 𝑧 = ⟨𝑗, 𝑘⟩))
71		eleq1w 2895	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑗 → (𝑚 ∈ {𝑦} ↔ 𝑗 ∈ {𝑦}))
72		velsn 4576	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ {𝑦} ↔ 𝑗 = 𝑦)
73	71, 72	syl6bb 289	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑗 → (𝑚 ∈ {𝑦} ↔ 𝑗 = 𝑦))
74	73	anbi1d 631	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑗 → ((𝑚 ∈ {𝑦} ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵) ↔ (𝑗 = 𝑦 ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵)))
75	22	eleq2d 2898	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑦 → (𝑘 ∈ 𝐵 ↔ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵))
76	75	pm5.32i 577	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵) ↔ (𝑗 = 𝑦 ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵))
77	74, 76	syl6bbr 291	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑗 → ((𝑚 ∈ {𝑦} ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵) ↔ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)))
78	70, 77	anbi12d 632	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑗 → ((𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵)) ↔ (𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵))))
79	78	exbidv 1918	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑗 → (∃𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵)) ↔ ∃𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵))))
80	67, 68, 79	cbvexv1 2358	. . . . . . . . . . . 12 ⊢ (∃𝑚∃𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵)) ↔ ∃𝑗∃𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)))
81	61, 80	bitri 277	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵) ↔ ∃𝑗∃𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)))
82		nfv 1911	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗𝜑
83		nfcv 2977	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗(2nd ‘𝑧)
84	83, 28	nfcsbw 3908	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶
85	84	nfeq2 2995	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗 𝐷 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶
86		nfv 1911	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘𝜑
87		nfcsb1v 3906	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶
88	87	nfeq2 2995	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘 𝐷 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶
89		fprod2d.1	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = ⟨𝑗, 𝑘⟩ → 𝐷 = 𝐶)
90	89	ad2antlr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)) → 𝐷 = 𝐶)
91	31	ad2antrl 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)) → 𝐶 = ⦋𝑦 / 𝑗⦌𝐶)
92		fveq2 6664	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ⟨𝑗, 𝑘⟩ → (2nd ‘𝑧) = (2nd ‘⟨𝑗, 𝑘⟩))
93		vex 3497	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑗 ∈ V
94		vex 3497	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑘 ∈ V
95	93, 94	op2nd 7692	. . . . . . . . . . . . . . . . . 18 ⊢ (2nd ‘⟨𝑗, 𝑘⟩) = 𝑘
96	92, 95	syl6req 2873	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ⟨𝑗, 𝑘⟩ → 𝑘 = (2nd ‘𝑧))
97	96	ad2antlr 725	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)) → 𝑘 = (2nd ‘𝑧))
98		csbeq1a 3896	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (2nd ‘𝑧) → ⦋𝑦 / 𝑗⦌𝐶 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶)
99	97, 98	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)) → ⦋𝑦 / 𝑗⦌𝐶 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶)
100	90, 91, 99	3eqtrd 2860	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)) → 𝐷 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶)
101	100	expl 460	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)) → 𝐷 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶))
102	86, 88, 101	exlimd 2214	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)) → 𝐷 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶))
103	82, 85, 102	exlimd 2214	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑗∃𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)) → 𝐷 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶))
104	81, 103	syl5bi 244	. . . . . . . . . 10 ⊢ (𝜑 → (𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵) → 𝐷 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶))
105	104	imp 409	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)) → 𝐷 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶)
106	105	prodeq2dv 15271	. . . . . . . 8 ⊢ (𝜑 → ∏𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)𝐷 = ∏𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶)
107	60, 106	eqtr4d 2859	. . . . . . 7 ⊢ (𝜑 → ∏𝑚 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑚 / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶 = ∏𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)𝐷)
108	47, 107	syl5eq 2868	. . . . . 6 ⊢ (𝜑 → ∏𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶 = ∏𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)𝐷)
109	43, 108	eqtrd 2856	. . . . 5 ⊢ (𝜑 → ∏𝑚 ∈ {𝑦}∏𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐶 = ∏𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)𝐷)
110	12, 109	syl5eq 2868	. . . 4 ⊢ (𝜑 → ∏𝑗 ∈ {𝑦}∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)𝐷)
111	110	adantr 483	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ∏𝑗 ∈ {𝑦}∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)𝐷)
112	3, 111	oveq12d 7168	. 2 ⊢ ((𝜑 ∧ 𝜓) → (∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 · ∏𝑗 ∈ {𝑦}∏𝑘 ∈ 𝐵 𝐶) = (∏𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷 · ∏𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)𝐷))
113		fprod2d.5	. . . . 5 ⊢ (𝜑 → ¬ 𝑦 ∈ 𝑥)
114		disjsn 4640	. . . . 5 ⊢ ((𝑥 ∩ {𝑦}) = ∅ ↔ ¬ 𝑦 ∈ 𝑥)
115	113, 114	sylibr 236	. . . 4 ⊢ (𝜑 → (𝑥 ∩ {𝑦}) = ∅)
116		eqidd 2822	. . . 4 ⊢ (𝜑 → (𝑥 ∪ {𝑦}) = (𝑥 ∪ {𝑦}))
117		fprod2d.2	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ Fin)
118	117, 13	ssfid 8735	. . . 4 ⊢ (𝜑 → (𝑥 ∪ {𝑦}) ∈ Fin)
119	13	sselda 3966	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) → 𝑗 ∈ 𝐴)
120	26	anassrs 470	. . . . . 6 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ)
121	18, 120	fprodcl 15300	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ∏𝑘 ∈ 𝐵 𝐶 ∈ ℂ)
122	119, 121	syldan 593	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) → ∏𝑘 ∈ 𝐵 𝐶 ∈ ℂ)
123	115, 116, 118, 122	fprodsplit 15314	. . 3 ⊢ (𝜑 → ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘 ∈ 𝐵 𝐶 = (∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 · ∏𝑗 ∈ {𝑦}∏𝑘 ∈ 𝐵 𝐶))
124	123	adantr 483	. 2 ⊢ ((𝜑 ∧ 𝜓) → ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘 ∈ 𝐵 𝐶 = (∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 · ∏𝑗 ∈ {𝑦}∏𝑘 ∈ 𝐵 𝐶))
125		eliun 4915	. . . . . . . . . 10 ⊢ (𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ↔ ∃𝑗 ∈ 𝑥 𝑧 ∈ ({𝑗} × 𝐵))
126		xp1st 7715	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ({𝑗} × 𝐵) → (1st ‘𝑧) ∈ {𝑗})
127		elsni 4577	. . . . . . . . . . . . . 14 ⊢ ((1st ‘𝑧) ∈ {𝑗} → (1st ‘𝑧) = 𝑗)
128	126, 127	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ ({𝑗} × 𝐵) → (1st ‘𝑧) = 𝑗)
129	128	eleq1d 2897	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ({𝑗} × 𝐵) → ((1st ‘𝑧) ∈ 𝑥 ↔ 𝑗 ∈ 𝑥))
130	129	biimparc 482	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ 𝑥 ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → (1st ‘𝑧) ∈ 𝑥)
131	130	rexlimiva 3281	. . . . . . . . . 10 ⊢ (∃𝑗 ∈ 𝑥 𝑧 ∈ ({𝑗} × 𝐵) → (1st ‘𝑧) ∈ 𝑥)
132	125, 131	sylbi 219	. . . . . . . . 9 ⊢ (𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) → (1st ‘𝑧) ∈ 𝑥)
133		xp1st 7715	. . . . . . . . 9 ⊢ (𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵) → (1st ‘𝑧) ∈ {𝑦})
134	132, 133	anim12i 614	. . . . . . . 8 ⊢ ((𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∧ 𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)) → ((1st ‘𝑧) ∈ 𝑥 ∧ (1st ‘𝑧) ∈ {𝑦}))
135		elin 4168	. . . . . . . 8 ⊢ (𝑧 ∈ (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)) ↔ (𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∧ 𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)))
136		elin 4168	. . . . . . . 8 ⊢ ((1st ‘𝑧) ∈ (𝑥 ∩ {𝑦}) ↔ ((1st ‘𝑧) ∈ 𝑥 ∧ (1st ‘𝑧) ∈ {𝑦}))
137	134, 135, 136	3imtr4i 294	. . . . . . 7 ⊢ (𝑧 ∈ (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)) → (1st ‘𝑧) ∈ (𝑥 ∩ {𝑦}))
138	115	eleq2d 2898	. . . . . . . 8 ⊢ (𝜑 → ((1st ‘𝑧) ∈ (𝑥 ∩ {𝑦}) ↔ (1st ‘𝑧) ∈ ∅))
139		noel 4295	. . . . . . . . 9 ⊢ ¬ (1st ‘𝑧) ∈ ∅
140	139	pm2.21i 119	. . . . . . . 8 ⊢ ((1st ‘𝑧) ∈ ∅ → 𝑧 ∈ ∅)
141	138, 140	syl6bi 255	. . . . . . 7 ⊢ (𝜑 → ((1st ‘𝑧) ∈ (𝑥 ∩ {𝑦}) → 𝑧 ∈ ∅))
142	137, 141	syl5 34	. . . . . 6 ⊢ (𝜑 → (𝑧 ∈ (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)) → 𝑧 ∈ ∅))
143	142	ssrdv 3972	. . . . 5 ⊢ (𝜑 → (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)) ⊆ ∅)
144		ss0 4351	. . . . 5 ⊢ ((∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)) ⊆ ∅ → (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)) = ∅)
145	143, 144	syl 17	. . . 4 ⊢ (𝜑 → (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)) = ∅)
146		iunxun 5008	. . . . . 6 ⊢ ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) = (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∪ ∪ 𝑗 ∈ {𝑦} ({𝑗} × 𝐵))
147		nfcv 2977	. . . . . . . . 9 ⊢ Ⅎ𝑚({𝑗} × 𝐵)
148		nfcv 2977	. . . . . . . . . 10 ⊢ Ⅎ𝑗{𝑚}
149	148, 5	nfxp 5582	. . . . . . . . 9 ⊢ Ⅎ𝑗({𝑚} × ⦋𝑚 / 𝑗⦌𝐵)
150		sneq 4570	. . . . . . . . . 10 ⊢ (𝑗 = 𝑚 → {𝑗} = {𝑚})
151	150, 8	xpeq12d 5580	. . . . . . . . 9 ⊢ (𝑗 = 𝑚 → ({𝑗} × 𝐵) = ({𝑚} × ⦋𝑚 / 𝑗⦌𝐵))
152	147, 149, 151	cbviun 4953	. . . . . . . 8 ⊢ ∪ 𝑗 ∈ {𝑦} ({𝑗} × 𝐵) = ∪ 𝑚 ∈ {𝑦} ({𝑚} × ⦋𝑚 / 𝑗⦌𝐵)
153		sneq 4570	. . . . . . . . . 10 ⊢ (𝑚 = 𝑦 → {𝑚} = {𝑦})
154	153, 38	xpeq12d 5580	. . . . . . . . 9 ⊢ (𝑚 = 𝑦 → ({𝑚} × ⦋𝑚 / 𝑗⦌𝐵) = ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵))
155	15, 154	iunxsn 5005	. . . . . . . 8 ⊢ ∪ 𝑚 ∈ {𝑦} ({𝑚} × ⦋𝑚 / 𝑗⦌𝐵) = ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)
156	152, 155	eqtri 2844	. . . . . . 7 ⊢ ∪ 𝑗 ∈ {𝑦} ({𝑗} × 𝐵) = ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)
157	156	uneq2i 4135	. . . . . 6 ⊢ (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∪ ∪ 𝑗 ∈ {𝑦} ({𝑗} × 𝐵)) = (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∪ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵))
158	146, 157	eqtri 2844	. . . . 5 ⊢ ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) = (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∪ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵))
159	158	a1i 11	. . . 4 ⊢ (𝜑 → ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) = (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∪ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)))
160		snfi 8588	. . . . . . 7 ⊢ {𝑗} ∈ Fin
161	119, 18	syldan 593	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) → 𝐵 ∈ Fin)
162		xpfi 8783	. . . . . . 7 ⊢ (({𝑗} ∈ Fin ∧ 𝐵 ∈ Fin) → ({𝑗} × 𝐵) ∈ Fin)
163	160, 161, 162	sylancr 589	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) → ({𝑗} × 𝐵) ∈ Fin)
164	163	ralrimiva 3182	. . . . 5 ⊢ (𝜑 → ∀𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ∈ Fin)
165		iunfi 8806	. . . . 5 ⊢ (((𝑥 ∪ {𝑦}) ∈ Fin ∧ ∀𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ∈ Fin) → ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ∈ Fin)
166	118, 164, 165	syl2anc 586	. . . 4 ⊢ (𝜑 → ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ∈ Fin)
167		eliun 4915	. . . . . 6 ⊢ (𝑧 ∈ ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ↔ ∃𝑗 ∈ (𝑥 ∪ {𝑦})𝑧 ∈ ({𝑗} × 𝐵))
168		elxp 5572	. . . . . . . 8 ⊢ (𝑧 ∈ ({𝑗} × 𝐵) ↔ ∃𝑚∃𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵)))
169		simprl 769	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → 𝑧 = ⟨𝑚, 𝑘⟩)
170		simprrl 779	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → 𝑚 ∈ {𝑗})
171		elsni 4577	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ {𝑗} → 𝑚 = 𝑗)
172	170, 171	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → 𝑚 = 𝑗)
173	172	opeq1d 4802	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → ⟨𝑚, 𝑘⟩ = ⟨𝑗, 𝑘⟩)
174	169, 173	eqtrd 2856	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → 𝑧 = ⟨𝑗, 𝑘⟩)
175	174, 89	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → 𝐷 = 𝐶)
176		simpll 765	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → 𝜑)
177	119	adantr 483	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → 𝑗 ∈ 𝐴)
178		simprrr 780	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → 𝑘 ∈ 𝐵)
179	176, 177, 178, 26	syl12anc 834	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → 𝐶 ∈ ℂ)
180	175, 179	eqeltrd 2913	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → 𝐷 ∈ ℂ)
181	180	ex 415	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) → ((𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵)) → 𝐷 ∈ ℂ))
182	181	exlimdvv 1931	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) → (∃𝑚∃𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵)) → 𝐷 ∈ ℂ))
183	168, 182	syl5bi 244	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) → (𝑧 ∈ ({𝑗} × 𝐵) → 𝐷 ∈ ℂ))
184	183	rexlimdva 3284	. . . . . 6 ⊢ (𝜑 → (∃𝑗 ∈ (𝑥 ∪ {𝑦})𝑧 ∈ ({𝑗} × 𝐵) → 𝐷 ∈ ℂ))
185	167, 184	syl5bi 244	. . . . 5 ⊢ (𝜑 → (𝑧 ∈ ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) → 𝐷 ∈ ℂ))
186	185	imp 409	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)) → 𝐷 ∈ ℂ)
187	145, 159, 166, 186	fprodsplit 15314	. . 3 ⊢ (𝜑 → ∏𝑧 ∈ ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷 = (∏𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷 · ∏𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)𝐷))
188	187	adantr 483	. 2 ⊢ ((𝜑 ∧ 𝜓) → ∏𝑧 ∈ ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷 = (∏𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷 · ∏𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)𝐷))
189	112, 124, 188	3eqtr4d 2866	1 ⊢ ((𝜑 ∧ 𝜓) → ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533  ∃wex 1776   ∈ wcel 2110  ∀wral 3138  ∃wrex 3139  ⦋csb 3882   ∪ cun 3933   ∩ cin 3934   ⊆ wss 3935  ∅c0 4290  {csn 4560  ⟨cop 4566  ∪ ciun 4911   × cxp 5547   ↾ cres 5551  –1-1-onto→wf1o 6348  ‘cfv 6349  (class class class)co 7150  1^st c1st 7681  2^nd c2nd 7682  Fincfn 8503  ℂcc 10529   · cmul 10536  ∏cprod 15253

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 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-inf2 9098  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608  ax-pre-sup 10609

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-fal 1546  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-tp 4565  df-op 4567  df-uni 4832  df-int 4869  df-iun 4913  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-se 5509  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-isom 6358  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7575  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-oadd 8100  df-er 8283  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-sup 8900  df-oi 8968  df-card 9362  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292  df-nn 11633  df-2 11694  df-3 11695  df-n0 11892  df-z 11976  df-uz 12238  df-rp 12384  df-fz 12887  df-fzo 13028  df-seq 13364  df-exp 13424  df-hash 13685  df-cj 14452  df-re 14453  df-im 14454  df-sqrt 14588  df-abs 14589  df-clim 14839  df-prod 15254

This theorem is referenced by:  fprod2d  15329