fprod2dlem

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

	Ref	Expression
Hypotheses	fprod2d.1	$⊢ z = ⟨j, k⟩ \to D = C$
	fprod2d.2	$⊢ φ \to A \in Fin$
	fprod2d.3	$⊢ (φ \land j \in A) \to B \in Fin$
	fprod2d.4	$⊢ (φ \land (j \in A \land k \in B)) \to C \in ℂ$
	fprod2d.5	$⊢ φ \to \neg y \in x$
	fprod2d.6	$⊢ φ \to x \cup \{y\} \subseteq A$
	fprod2d.7	$⊢ ψ \leftrightarrow \prod_{j \in x} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x} (\{j\} \times B)} D$
Assertion	fprod2dlem	$⊢ (φ \land ψ) \to \prod_{j \in x \cup \{y\}} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D$

Proof

Step	Hyp	Ref	Expression
1		fprod2d.1	$⊢ z = ⟨j, k⟩ \to D = C$
2		fprod2d.2	$⊢ φ \to A \in Fin$
3		fprod2d.3	$⊢ (φ \land j \in A) \to B \in Fin$
4		fprod2d.4	$⊢ (φ \land (j \in A \land k \in B)) \to C \in ℂ$
5		fprod2d.5	$⊢ φ \to \neg y \in x$
6		fprod2d.6	$⊢ φ \to x \cup \{y\} \subseteq A$
7		fprod2d.7	$⊢ ψ \leftrightarrow \prod_{j \in x} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x} (\{j\} \times B)} D$
8	7	bilani	$⊢ (φ \land ψ) \to \prod_{j \in x} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x} (\{j\} \times B)} D$
9		nfcv	$⊢ \underline{Ⅎ} m \prod_{k \in B} C$
10		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ m / j ⦌ B$
11		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ m / j ⦌ C$
12	10 11	nfcprod	$⊢ \underline{Ⅎ} j \prod_{k \in ⦋ m / j ⦌ B} ⦋ m / j ⦌ C$
13		csbeq1a	$⊢ j = m \to B = ⦋ m / j ⦌ B$
14		csbeq1a	$⊢ j = m \to C = ⦋ m / j ⦌ C$
15	14	adantr	$⊢ (j = m \land k \in B) \to C = ⦋ m / j ⦌ C$
16	13 15	prodeq12dv	$⊢ j = m \to \prod_{k \in B} C = \prod_{k \in ⦋ m / j ⦌ B} ⦋ m / j ⦌ C$
17	9 12 16	cbvprodi	$⊢ \prod_{j \in \{y\}} \prod_{k \in B} C = \prod_{m \in \{y\}} \prod_{k \in ⦋ m / j ⦌ B} ⦋ m / j ⦌ C$
18	6	unssbd	$⊢ φ \to \{y\} \subseteq A$
19		vex	$⊢ y \in V$
20	19	snss	$⊢ y \in A \leftrightarrow \{y\} \subseteq A$
21	18 20	sylibr	$⊢ φ \to y \in A$
22	3	ralrimiva	$⊢ φ \to \forall j \in A B \in Fin$
23		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ y / j ⦌ B$
24	23	nfel1	$⊢ Ⅎ j ⦋ y / j ⦌ B \in Fin$
25		csbeq1a	$⊢ j = y \to B = ⦋ y / j ⦌ B$
26	25	eleq1d	$⊢ j = y \to (B \in Fin \leftrightarrow ⦋ y / j ⦌ B \in Fin)$
27	24 26	rspc	$⊢ y \in A \to (\forall j \in A B \in Fin \to ⦋ y / j ⦌ B \in Fin)$
28	21 22 27	sylc	$⊢ φ \to ⦋ y / j ⦌ B \in Fin$
29	4	ralrimivva	$⊢ φ \to \forall j \in A \forall k \in B C \in ℂ$
30		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ y / j ⦌ C$
31	30	nfel1	$⊢ Ⅎ j ⦋ y / j ⦌ C \in ℂ$
32	23 31	nfralw	$⊢ Ⅎ j \forall k \in ⦋ y / j ⦌ B ⦋ y / j ⦌ C \in ℂ$
33		csbeq1a	$⊢ j = y \to C = ⦋ y / j ⦌ C$
34	33	eleq1d	$⊢ j = y \to (C \in ℂ \leftrightarrow ⦋ y / j ⦌ C \in ℂ)$
35	25 34	raleqbidv	$⊢ j = y \to (\forall k \in B C \in ℂ \leftrightarrow \forall k \in ⦋ y / j ⦌ B ⦋ y / j ⦌ C \in ℂ)$
36	32 35	rspc	$⊢ y \in A \to (\forall j \in A \forall k \in B C \in ℂ \to \forall k \in ⦋ y / j ⦌ B ⦋ y / j ⦌ C \in ℂ)$
37	21 29 36	sylc	$⊢ φ \to \forall k \in ⦋ y / j ⦌ B ⦋ y / j ⦌ C \in ℂ$
38	37	r19.21bi	$⊢ (φ \land k \in ⦋ y / j ⦌ B) \to ⦋ y / j ⦌ C \in ℂ$
39	28 38	fprodcl	$⊢ φ \to \prod_{k \in ⦋ y / j ⦌ B} ⦋ y / j ⦌ C \in ℂ$
40		csbeq1	$⊢ m = y \to ⦋ m / j ⦌ B = ⦋ y / j ⦌ B$
41		csbeq1	$⊢ m = y \to ⦋ m / j ⦌ C = ⦋ y / j ⦌ C$
42	41	adantr	$⊢ (m = y \land k \in ⦋ m / j ⦌ B) \to ⦋ m / j ⦌ C = ⦋ y / j ⦌ C$
43	40 42	prodeq12dv	$⊢ m = y \to \prod_{k \in ⦋ m / j ⦌ B} ⦋ m / j ⦌ C = \prod_{k \in ⦋ y / j ⦌ B} ⦋ y / j ⦌ C$
44	43	prodsn	$⊢ (y \in A \land \prod_{k \in ⦋ y / j ⦌ B} ⦋ y / j ⦌ C \in ℂ) \to \prod_{m \in \{y\}} \prod_{k \in ⦋ m / j ⦌ B} ⦋ m / j ⦌ C = \prod_{k \in ⦋ y / j ⦌ B} ⦋ y / j ⦌ C$
45	21 39 44	syl2anc	$⊢ φ \to \prod_{m \in \{y\}} \prod_{k \in ⦋ m / j ⦌ B} ⦋ m / j ⦌ C = \prod_{k \in ⦋ y / j ⦌ B} ⦋ y / j ⦌ C$
46		nfcv	$⊢ \underline{Ⅎ} m ⦋ y / j ⦌ C$
47		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ m / k ⦌ ⦋ y / j ⦌ C$
48		csbeq1a	$⊢ k = m \to ⦋ y / j ⦌ C = ⦋ m / k ⦌ ⦋ y / j ⦌ C$
49	46 47 48	cbvprodi	$⊢ \prod_{k \in ⦋ y / j ⦌ B} ⦋ y / j ⦌ C = \prod_{m \in ⦋ y / j ⦌ B} ⦋ m / k ⦌ ⦋ y / j ⦌ C$
50		csbeq1	$⊢ m = 2^{nd} (z) \to ⦋ m / k ⦌ ⦋ y / j ⦌ C = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
51		snfi	$⊢ \{y\} \in Fin$
52		xpfi	$⊢ (\{y\} \in Fin \land ⦋ y / j ⦌ B \in Fin) \to \{y\} \times ⦋ y / j ⦌ B \in Fin$
53	51 28 52	sylancr	$⊢ φ \to \{y\} \times ⦋ y / j ⦌ B \in Fin$
54		2ndconst	$⊢ y \in A \to ({2^{nd} ↾}_{(\{y\} \times ⦋ y / j ⦌ B)}) : \{y\} \times ⦋ y / j ⦌ B \underset{1-1 onto}{⟶} ⦋ y / j ⦌ B$
55	21 54	syl	$⊢ φ \to ({2^{nd} ↾}_{(\{y\} \times ⦋ y / j ⦌ B)}) : \{y\} \times ⦋ y / j ⦌ B \underset{1-1 onto}{⟶} ⦋ y / j ⦌ B$
56		fvres	$⊢ z \in (\{y\} \times ⦋ y / j ⦌ B) \to ({2^{nd} ↾}_{(\{y\} \times ⦋ y / j ⦌ B)}) (z) = 2^{nd} (z)$
57	56	adantl	$⊢ (φ \land z \in (\{y\} \times ⦋ y / j ⦌ B)) \to ({2^{nd} ↾}_{(\{y\} \times ⦋ y / j ⦌ B)}) (z) = 2^{nd} (z)$
58	47	nfel1	$⊢ Ⅎ k ⦋ m / k ⦌ ⦋ y / j ⦌ C \in ℂ$
59	48	eleq1d	$⊢ k = m \to (⦋ y / j ⦌ C \in ℂ \leftrightarrow ⦋ m / k ⦌ ⦋ y / j ⦌ C \in ℂ)$
60	58 59	rspc	$⊢ m \in ⦋ y / j ⦌ B \to (\forall k \in ⦋ y / j ⦌ B ⦋ y / j ⦌ C \in ℂ \to ⦋ m / k ⦌ ⦋ y / j ⦌ C \in ℂ)$
61	37 60	mpan9	$⊢ (φ \land m \in ⦋ y / j ⦌ B) \to ⦋ m / k ⦌ ⦋ y / j ⦌ C \in ℂ$
62	50 53 55 57 61	fprodf1o	$⊢ φ \to \prod_{m \in ⦋ y / j ⦌ B} ⦋ m / k ⦌ ⦋ y / j ⦌ C = \prod_{z \in \{y\} \times ⦋ y / j ⦌ B} ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
63		elxp	$⊢ z \in (\{y\} \times ⦋ y / j ⦌ B) \leftrightarrow \exists m \exists k (z = ⟨m, k⟩ \land (m \in \{y\} \land k \in ⦋ y / j ⦌ B))$
64		nfv	$⊢ Ⅎ j z = ⟨m, k⟩$
65		nfv	$⊢ Ⅎ j m \in \{y\}$
66	23	nfcri	$⊢ Ⅎ j k \in ⦋ y / j ⦌ B$
67	65 66	nfan	$⊢ Ⅎ j (m \in \{y\} \land k \in ⦋ y / j ⦌ B)$
68	64 67	nfan	$⊢ Ⅎ j (z = ⟨m, k⟩ \land (m \in \{y\} \land k \in ⦋ y / j ⦌ B))$
69	68	nfex	$⊢ Ⅎ j \exists k (z = ⟨m, k⟩ \land (m \in \{y\} \land k \in ⦋ y / j ⦌ B))$
70		nfv	$⊢ Ⅎ m \exists k (z = ⟨j, k⟩ \land (j = y \land k \in B))$
71		opeq1	$⊢ m = j \to ⟨m, k⟩ = ⟨j, k⟩$
72	71	eqeq2d	$⊢ m = j \to (z = ⟨m, k⟩ \leftrightarrow z = ⟨j, k⟩)$
73		eleq1w	$⊢ m = j \to (m \in \{y\} \leftrightarrow j \in \{y\})$
74		velsn	$⊢ j \in \{y\} \leftrightarrow j = y$
75	73 74	bitrdi	$⊢ m = j \to (m \in \{y\} \leftrightarrow j = y)$
76	75	anbi1d	$⊢ m = j \to ((m \in \{y\} \land k \in ⦋ y / j ⦌ B) \leftrightarrow (j = y \land k \in ⦋ y / j ⦌ B))$
77	25	eleq2d	$⊢ j = y \to (k \in B \leftrightarrow k \in ⦋ y / j ⦌ B)$
78	77	pm5.32i	$⊢ (j = y \land k \in B) \leftrightarrow (j = y \land k \in ⦋ y / j ⦌ B)$
79	76 78	bitr4di	$⊢ m = j \to ((m \in \{y\} \land k \in ⦋ y / j ⦌ B) \leftrightarrow (j = y \land k \in B))$
80	72 79	anbi12d	$⊢ m = j \to ((z = ⟨m, k⟩ \land (m \in \{y\} \land k \in ⦋ y / j ⦌ B)) \leftrightarrow (z = ⟨j, k⟩ \land (j = y \land k \in B)))$
81	80	exbidv	$⊢ m = j \to (\exists k (z = ⟨m, k⟩ \land (m \in \{y\} \land k \in ⦋ y / j ⦌ B)) \leftrightarrow \exists k (z = ⟨j, k⟩ \land (j = y \land k \in B)))$
82	69 70 81	cbvexv1	$⊢ \exists m \exists k (z = ⟨m, k⟩ \land (m \in \{y\} \land k \in ⦋ y / j ⦌ B)) \leftrightarrow \exists j \exists k (z = ⟨j, k⟩ \land (j = y \land k \in B))$
83	63 82	bitri	$⊢ z \in (\{y\} \times ⦋ y / j ⦌ B) \leftrightarrow \exists j \exists k (z = ⟨j, k⟩ \land (j = y \land k \in B))$
84		nfv	$⊢ Ⅎ j φ$
85		nfcv	$⊢ \underline{Ⅎ} j 2^{nd} (z)$
86	85 30	nfcsbw	$⊢ \underline{Ⅎ} j ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
87	86	nfeq2	$⊢ Ⅎ j D = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
88		nfv	$⊢ Ⅎ k φ$
89		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
90	89	nfeq2	$⊢ Ⅎ k D = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
91	1	ad2antlr	$⊢ ((φ \land z = ⟨j, k⟩) \land (j = y \land k \in B)) \to D = C$
92	33	ad2antrl	$⊢ ((φ \land z = ⟨j, k⟩) \land (j = y \land k \in B)) \to C = ⦋ y / j ⦌ C$
93		fveq2	$⊢ z = ⟨j, k⟩ \to 2^{nd} (z) = 2^{nd} (⟨j, k⟩)$
94		vex	$⊢ j \in V$
95		vex	$⊢ k \in V$
96	94 95	op2nd	$⊢ 2^{nd} (⟨j, k⟩) = k$
97	93 96	eqtr2di	$⊢ z = ⟨j, k⟩ \to k = 2^{nd} (z)$
98	97	ad2antlr	$⊢ ((φ \land z = ⟨j, k⟩) \land (j = y \land k \in B)) \to k = 2^{nd} (z)$
99		csbeq1a	$⊢ k = 2^{nd} (z) \to ⦋ y / j ⦌ C = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
100	98 99	syl	$⊢ ((φ \land z = ⟨j, k⟩) \land (j = y \land k \in B)) \to ⦋ y / j ⦌ C = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
101	91 92 100	3eqtrd	$⊢ ((φ \land z = ⟨j, k⟩) \land (j = y \land k \in B)) \to D = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
102	101	expl	$⊢ φ \to ((z = ⟨j, k⟩ \land (j = y \land k \in B)) \to D = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C)$
103	88 90 102	exlimd	$⊢ φ \to (\exists k (z = ⟨j, k⟩ \land (j = y \land k \in B)) \to D = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C)$
104	84 87 103	exlimd	$⊢ φ \to (\exists j \exists k (z = ⟨j, k⟩ \land (j = y \land k \in B)) \to D = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C)$
105	83 104	biimtrid	$⊢ φ \to (z \in (\{y\} \times ⦋ y / j ⦌ B) \to D = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C)$
106	105	imp	$⊢ (φ \land z \in (\{y\} \times ⦋ y / j ⦌ B)) \to D = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
107	106	prodeq2dv	$⊢ φ \to \prod_{z \in \{y\} \times ⦋ y / j ⦌ B} D = \prod_{z \in \{y\} \times ⦋ y / j ⦌ B} ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
108	62 107	eqtr4d	$⊢ φ \to \prod_{m \in ⦋ y / j ⦌ B} ⦋ m / k ⦌ ⦋ y / j ⦌ C = \prod_{z \in \{y\} \times ⦋ y / j ⦌ B} D$
109	49 108	eqtrid	$⊢ φ \to \prod_{k \in ⦋ y / j ⦌ B} ⦋ y / j ⦌ C = \prod_{z \in \{y\} \times ⦋ y / j ⦌ B} D$
110	45 109	eqtrd	$⊢ φ \to \prod_{m \in \{y\}} \prod_{k \in ⦋ m / j ⦌ B} ⦋ m / j ⦌ C = \prod_{z \in \{y\} \times ⦋ y / j ⦌ B} D$
111	17 110	eqtrid	$⊢ φ \to \prod_{j \in \{y\}} \prod_{k \in B} C = \prod_{z \in \{y\} \times ⦋ y / j ⦌ B} D$
112	111	adantr	$⊢ (φ \land ψ) \to \prod_{j \in \{y\}} \prod_{k \in B} C = \prod_{z \in \{y\} \times ⦋ y / j ⦌ B} D$
113	8 112	oveq12d	$⊢ (φ \land ψ) \to \prod_{j \in x} \prod_{k \in B} C \prod_{j \in \{y\}} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x} (\{j\} \times B)} D \prod_{z \in \{y\} \times ⦋ y / j ⦌ B} D$
114		disjsn	$⊢ x \cap \{y\} = \emptyset \leftrightarrow \neg y \in x$
115	5 114	sylibr	$⊢ φ \to x \cap \{y\} = \emptyset$
116		eqidd	$⊢ φ \to x \cup \{y\} = x \cup \{y\}$
117	2 6	ssfid	$⊢ φ \to x \cup \{y\} \in Fin$
118	6	sselda	$⊢ (φ \land j \in (x \cup \{y\})) \to j \in A$
119	4	anassrs	$⊢ ((φ \land j \in A) \land k \in B) \to C \in ℂ$
120	3 119	fprodcl	$⊢ (φ \land j \in A) \to \prod_{k \in B} C \in ℂ$
121	118 120	syldan	$⊢ (φ \land j \in (x \cup \{y\})) \to \prod_{k \in B} C \in ℂ$
122	115 116 117 121	fprodsplit	$⊢ φ \to \prod_{j \in x \cup \{y\}} \prod_{k \in B} C = \prod_{j \in x} \prod_{k \in B} C \prod_{j \in \{y\}} \prod_{k \in B} C$
123	122	adantr	$⊢ (φ \land ψ) \to \prod_{j \in x \cup \{y\}} \prod_{k \in B} C = \prod_{j \in x} \prod_{k \in B} C \prod_{j \in \{y\}} \prod_{k \in B} C$
124		eliun	$⊢ z \in ⋃_{j \in x} (\{j\} \times B) \leftrightarrow \exists j \in x z \in (\{j\} \times B)$
125		xp1st	$⊢ z \in (\{j\} \times B) \to 1^{st} (z) \in \{j\}$
126		elsni	$⊢ 1^{st} (z) \in \{j\} \to 1^{st} (z) = j$
127	125 126	syl	$⊢ z \in (\{j\} \times B) \to 1^{st} (z) = j$
128	127	eleq1d	$⊢ z \in (\{j\} \times B) \to (1^{st} (z) \in x \leftrightarrow j \in x)$
129	128	biimparc	$⊢ (j \in x \land z \in (\{j\} \times B)) \to 1^{st} (z) \in x$
130	129	rexlimiva	$⊢ \exists j \in x z \in (\{j\} \times B) \to 1^{st} (z) \in x$
131	124 130	sylbi	$⊢ z \in ⋃_{j \in x} (\{j\} \times B) \to 1^{st} (z) \in x$
132		xp1st	$⊢ z \in (\{y\} \times ⦋ y / j ⦌ B) \to 1^{st} (z) \in \{y\}$
133	131 132	anim12i	$⊢ (z \in ⋃_{j \in x} (\{j\} \times B) \land z \in (\{y\} \times ⦋ y / j ⦌ B)) \to (1^{st} (z) \in x \land 1^{st} (z) \in \{y\})$
134		elin	$⊢ z \in (⋃_{j \in x} (\{j\} \times B) \cap (\{y\} \times ⦋ y / j ⦌ B)) \leftrightarrow (z \in ⋃_{j \in x} (\{j\} \times B) \land z \in (\{y\} \times ⦋ y / j ⦌ B))$
135		elin	$⊢ 1^{st} (z) \in (x \cap \{y\}) \leftrightarrow (1^{st} (z) \in x \land 1^{st} (z) \in \{y\})$
136	133 134 135	3imtr4i	$⊢ z \in (⋃_{j \in x} (\{j\} \times B) \cap (\{y\} \times ⦋ y / j ⦌ B)) \to 1^{st} (z) \in (x \cap \{y\})$
137	115	eleq2d	$⊢ φ \to (1^{st} (z) \in (x \cap \{y\}) \leftrightarrow 1^{st} (z) \in \emptyset)$
138		noel	$⊢ \neg 1^{st} (z) \in \emptyset$
139	138	pm2.21i	$⊢ 1^{st} (z) \in \emptyset \to z \in \emptyset$
140	137 139	biimtrdi	$⊢ φ \to (1^{st} (z) \in (x \cap \{y\}) \to z \in \emptyset)$
141	136 140	syl5	$⊢ φ \to (z \in (⋃_{j \in x} (\{j\} \times B) \cap (\{y\} \times ⦋ y / j ⦌ B)) \to z \in \emptyset)$
142	141	ssrdv	$⊢ φ \to ⋃_{j \in x} (\{j\} \times B) \cap (\{y\} \times ⦋ y / j ⦌ B) \subseteq \emptyset$
143		ss0	$⊢ ⋃_{j \in x} (\{j\} \times B) \cap (\{y\} \times ⦋ y / j ⦌ B) \subseteq \emptyset \to ⋃_{j \in x} (\{j\} \times B) \cap (\{y\} \times ⦋ y / j ⦌ B) = \emptyset$
144	142 143	syl	$⊢ φ \to ⋃_{j \in x} (\{j\} \times B) \cap (\{y\} \times ⦋ y / j ⦌ B) = \emptyset$
145		iunxun	$⊢ ⋃_{j \in x \cup \{y\}} (\{j\} \times B) = ⋃_{j \in x} (\{j\} \times B) \cup ⋃_{j \in \{y\}} (\{j\} \times B)$
146		nfcv	$⊢ \underline{Ⅎ} m (\{j\} \times B)$
147		nfcv	$⊢ \underline{Ⅎ} j \{m\}$
148	147 10	nfxp	$⊢ \underline{Ⅎ} j (\{m\} \times ⦋ m / j ⦌ B)$
149		sneq	$⊢ j = m \to \{j\} = \{m\}$
150	149 13	xpeq12d	$⊢ j = m \to \{j\} \times B = \{m\} \times ⦋ m / j ⦌ B$
151	146 148 150	cbviun	$⊢ ⋃_{j \in \{y\}} (\{j\} \times B) = ⋃_{m \in \{y\}} (\{m\} \times ⦋ m / j ⦌ B)$
152		sneq	$⊢ m = y \to \{m\} = \{y\}$
153	152 40	xpeq12d	$⊢ m = y \to \{m\} \times ⦋ m / j ⦌ B = \{y\} \times ⦋ y / j ⦌ B$
154	19 153	iunxsn	$⊢ ⋃_{m \in \{y\}} (\{m\} \times ⦋ m / j ⦌ B) = \{y\} \times ⦋ y / j ⦌ B$
155	151 154	eqtri	$⊢ ⋃_{j \in \{y\}} (\{j\} \times B) = \{y\} \times ⦋ y / j ⦌ B$
156	155	uneq2i	$⊢ ⋃_{j \in x} (\{j\} \times B) \cup ⋃_{j \in \{y\}} (\{j\} \times B) = ⋃_{j \in x} (\{j\} \times B) \cup (\{y\} \times ⦋ y / j ⦌ B)$
157	145 156	eqtri	$⊢ ⋃_{j \in x \cup \{y\}} (\{j\} \times B) = ⋃_{j \in x} (\{j\} \times B) \cup (\{y\} \times ⦋ y / j ⦌ B)$
158	157	a1i	$⊢ φ \to ⋃_{j \in x \cup \{y\}} (\{j\} \times B) = ⋃_{j \in x} (\{j\} \times B) \cup (\{y\} \times ⦋ y / j ⦌ B)$
159		snfi	$⊢ \{j\} \in Fin$
160	118 3	syldan	$⊢ (φ \land j \in (x \cup \{y\})) \to B \in Fin$
161		xpfi	$⊢ (\{j\} \in Fin \land B \in Fin) \to \{j\} \times B \in Fin$
162	159 160 161	sylancr	$⊢ (φ \land j \in (x \cup \{y\})) \to \{j\} \times B \in Fin$
163	162	ralrimiva	$⊢ φ \to \forall j \in (x \cup \{y\}) \{j\} \times B \in Fin$
164		iunfi	$⊢ (x \cup \{y\} \in Fin \land \forall j \in (x \cup \{y\}) \{j\} \times B \in Fin) \to ⋃_{j \in x \cup \{y\}} (\{j\} \times B) \in Fin$
165	117 163 164	syl2anc	$⊢ φ \to ⋃_{j \in x \cup \{y\}} (\{j\} \times B) \in Fin$
166		eliun	$⊢ z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B) \leftrightarrow \exists j \in (x \cup \{y\}) z \in (\{j\} \times B)$
167		elxp	$⊢ z \in (\{j\} \times B) \leftrightarrow \exists m \exists k (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))$
168		simprl	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to z = ⟨m, k⟩$
169		simprrl	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to m \in \{j\}$
170		elsni	$⊢ m \in \{j\} \to m = j$
171	169 170	syl	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to m = j$
172	171	opeq1d	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to ⟨m, k⟩ = ⟨j, k⟩$
173	168 172	eqtrd	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to z = ⟨j, k⟩$
174	173 1	syl	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to D = C$
175		simpll	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to φ$
176	118	adantr	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to j \in A$
177		simprrr	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to k \in B$
178	175 176 177 4	syl12anc	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to C \in ℂ$
179	174 178	eqeltrd	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to D \in ℂ$
180	179	ex	$⊢ (φ \land j \in (x \cup \{y\})) \to ((z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B)) \to D \in ℂ)$
181	180	exlimdvv	$⊢ (φ \land j \in (x \cup \{y\})) \to (\exists m \exists k (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B)) \to D \in ℂ)$
182	167 181	biimtrid	$⊢ (φ \land j \in (x \cup \{y\})) \to (z \in (\{j\} \times B) \to D \in ℂ)$
183	182	rexlimdva	$⊢ φ \to (\exists j \in (x \cup \{y\}) z \in (\{j\} \times B) \to D \in ℂ)$
184	166 183	biimtrid	$⊢ φ \to (z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B) \to D \in ℂ)$
185	184	imp	$⊢ (φ \land z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)) \to D \in ℂ$
186	144 158 165 185	fprodsplit	$⊢ φ \to \prod_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D = \prod_{z \in ⋃_{j \in x} (\{j\} \times B)} D \prod_{z \in \{y\} \times ⦋ y / j ⦌ B} D$
187	186	adantr	$⊢ (φ \land ψ) \to \prod_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D = \prod_{z \in ⋃_{j \in x} (\{j\} \times B)} D \prod_{z \in \{y\} \times ⦋ y / j ⦌ B} D$
188	113 123 187	3eqtr4d	$⊢ (φ \land ψ) \to \prod_{j \in x \cup \{y\}} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D$

Metamath Proof Explorer

Theorem fprod2dlem

Proof