csbfinxpg

Description: Distribute proper substitution through Cartesian exponentiation. (Contributed by ML, 25-Oct-2020)

		Ref	Expression
	Assertion	csbfinxpg	$⊢ A \in V \to ⦋ A / x ⦌ U ↑↑ N = ⦋ A / x ⦌ U ↑↑ ⦋ A / x ⦌ N$

Proof

Step	Hyp	Ref	Expression
1		df-finxp	$⊢ U ↑↑ N = \{y \| (N \in ω \land \emptyset = rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in U), \emptyset, if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨N, y⟩) (N))\}$
2	1	csbeq2i	$⊢ ⦋ A / x ⦌ U ↑↑ N = ⦋ A / x ⦌ \{y \| (N \in ω \land \emptyset = rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in U), \emptyset, if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨N, y⟩) (N))\}$
3		sbcan	$⊢ \underset{˙}{[} A / x \underset{˙}{]} (N \in ω \land \emptyset = rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in U), \emptyset, if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨N, y⟩) (N)) \leftrightarrow (\underset{˙}{[} A / x \underset{˙}{]} N \in ω \land \underset{˙}{[} A / x \underset{˙}{]} \emptyset = rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in U), \emptyset, if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨N, y⟩) (N))$
4		sbcel1g	$⊢ A \in V \to (\underset{˙}{[} A / x \underset{˙}{]} N \in ω \leftrightarrow ⦋ A / x ⦌ N \in ω)$
5		sbceq2g	$⊢ A \in V \to (\underset{˙}{[} A / x \underset{˙}{]} \emptyset = rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in U), \emptyset, if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨N, y⟩) (N) \leftrightarrow \emptyset = ⦋ A / x ⦌ rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in U), \emptyset, if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨N, y⟩) (N))$
6		csbfv12	$⊢ ⦋ A / x ⦌ rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in U), \emptyset, if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨N, y⟩) (N) = ⦋ A / x ⦌ rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in U), \emptyset, if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨N, y⟩) (⦋ A / x ⦌ N)$
7		csbrdgg	$⊢ A \in V \to ⦋ A / x ⦌ rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in U), \emptyset, if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨N, y⟩) = rec (⦋ A / x ⦌ (n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in U), \emptyset, if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⦋ A / x ⦌ ⟨N, y⟩)$
8		csbmpo123	$⊢ A \in V \to ⦋ A / x ⦌ (n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in U), \emptyset, if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))) = (n \in ⦋ A / x ⦌ ω, z \in ⦋ A / x ⦌ V ⟼ ⦋ A / x ⦌ if ((n = 1_{𝑜} \land z \in U), \emptyset, if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩)))$
9		csbconstg	$⊢ A \in V \to ⦋ A / x ⦌ ω = ω$
10		csbconstg	$⊢ A \in V \to ⦋ A / x ⦌ V = V$
11		csbif	$⊢ ⦋ A / x ⦌ if ((n = 1_{𝑜} \land z \in U), \emptyset, if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩)) = if (\underset{˙}{[} A / x \underset{˙}{]} (n = 1_{𝑜} \land z \in U), ⦋ A / x ⦌ \emptyset, ⦋ A / x ⦌ if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))$
12		sbcan	$⊢ \underset{˙}{[} A / x \underset{˙}{]} (n = 1_{𝑜} \land z \in U) \leftrightarrow (\underset{˙}{[} A / x \underset{˙}{]} n = 1_{𝑜} \land \underset{˙}{[} A / x \underset{˙}{]} z \in U)$
13		sbcg	$⊢ A \in V \to (\underset{˙}{[} A / x \underset{˙}{]} n = 1_{𝑜} \leftrightarrow n = 1_{𝑜})$
14		sbcel12	$⊢ \underset{˙}{[} A / x \underset{˙}{]} z \in U \leftrightarrow ⦋ A / x ⦌ z \in ⦋ A / x ⦌ U$
15		csbconstg	$⊢ A \in V \to ⦋ A / x ⦌ z = z$
16	15	eleq1d	$⊢ A \in V \to (⦋ A / x ⦌ z \in ⦋ A / x ⦌ U \leftrightarrow z \in ⦋ A / x ⦌ U)$
17	14 16	syl5bb	$⊢ A \in V \to (\underset{˙}{[} A / x \underset{˙}{]} z \in U \leftrightarrow z \in ⦋ A / x ⦌ U)$
18	13 17	anbi12d	$⊢ A \in V \to ((\underset{˙}{[} A / x \underset{˙}{]} n = 1_{𝑜} \land \underset{˙}{[} A / x \underset{˙}{]} z \in U) \leftrightarrow (n = 1_{𝑜} \land z \in ⦋ A / x ⦌ U))$
19	12 18	syl5bb	$⊢ A \in V \to (\underset{˙}{[} A / x \underset{˙}{]} (n = 1_{𝑜} \land z \in U) \leftrightarrow (n = 1_{𝑜} \land z \in ⦋ A / x ⦌ U))$
20		csbconstg	$⊢ A \in V \to ⦋ A / x ⦌ \emptyset = \emptyset$
21		csbif	$⊢ ⦋ A / x ⦌ if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩) = if (\underset{˙}{[} A / x \underset{˙}{]} z \in (V \times U), ⦋ A / x ⦌ ⟨⋃ n, 1^{st} (z)⟩, ⦋ A / x ⦌ ⟨n, z⟩)$
22		sbcel12	$⊢ \underset{˙}{[} A / x \underset{˙}{]} z \in (V \times U) \leftrightarrow ⦋ A / x ⦌ z \in ⦋ A / x ⦌ (V \times U)$
23		csbxp	$⊢ ⦋ A / x ⦌ (V \times U) = ⦋ A / x ⦌ V \times ⦋ A / x ⦌ U$
24	10	xpeq1d	$⊢ A \in V \to ⦋ A / x ⦌ V \times ⦋ A / x ⦌ U = V \times ⦋ A / x ⦌ U$
25	23 24	syl5eq	$⊢ A \in V \to ⦋ A / x ⦌ (V \times U) = V \times ⦋ A / x ⦌ U$
26	15 25	eleq12d	$⊢ A \in V \to (⦋ A / x ⦌ z \in ⦋ A / x ⦌ (V \times U) \leftrightarrow z \in (V \times ⦋ A / x ⦌ U))$
27	22 26	syl5bb	$⊢ A \in V \to (\underset{˙}{[} A / x \underset{˙}{]} z \in (V \times U) \leftrightarrow z \in (V \times ⦋ A / x ⦌ U))$
28		csbconstg	$⊢ A \in V \to ⦋ A / x ⦌ ⟨⋃ n, 1^{st} (z)⟩ = ⟨⋃ n, 1^{st} (z)⟩$
29		csbconstg	$⊢ A \in V \to ⦋ A / x ⦌ ⟨n, z⟩ = ⟨n, z⟩$
30	27 28 29	ifbieq12d	$⊢ A \in V \to if (\underset{˙}{[} A / x \underset{˙}{]} z \in (V \times U), ⦋ A / x ⦌ ⟨⋃ n, 1^{st} (z)⟩, ⦋ A / x ⦌ ⟨n, z⟩) = if (z \in (V \times ⦋ A / x ⦌ U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩)$
31	21 30	syl5eq	$⊢ A \in V \to ⦋ A / x ⦌ if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩) = if (z \in (V \times ⦋ A / x ⦌ U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩)$
32	19 20 31	ifbieq12d	$⊢ A \in V \to if (\underset{˙}{[} A / x \underset{˙}{]} (n = 1_{𝑜} \land z \in U), ⦋ A / x ⦌ \emptyset, ⦋ A / x ⦌ if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩)) = if ((n = 1_{𝑜} \land z \in ⦋ A / x ⦌ U), \emptyset, if (z \in (V \times ⦋ A / x ⦌ U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))$
33	11 32	syl5eq	$⊢ A \in V \to ⦋ A / x ⦌ if ((n = 1_{𝑜} \land z \in U), \emptyset, if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩)) = if ((n = 1_{𝑜} \land z \in ⦋ A / x ⦌ U), \emptyset, if (z \in (V \times ⦋ A / x ⦌ U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))$
34	9 10 33	mpoeq123dv	$⊢ A \in V \to (n \in ⦋ A / x ⦌ ω, z \in ⦋ A / x ⦌ V ⟼ ⦋ A / x ⦌ if ((n = 1_{𝑜} \land z \in U), \emptyset, if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))) = (n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in ⦋ A / x ⦌ U), \emptyset, if (z \in (V \times ⦋ A / x ⦌ U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩)))$
35	8 34	eqtrd	$⊢ A \in V \to ⦋ A / x ⦌ (n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in U), \emptyset, if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))) = (n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in ⦋ A / x ⦌ U), \emptyset, if (z \in (V \times ⦋ A / x ⦌ U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩)))$
36		csbopg	$⊢ A \in V \to ⦋ A / x ⦌ ⟨N, y⟩ = ⟨⦋ A / x ⦌ N, ⦋ A / x ⦌ y⟩$
37		csbconstg	$⊢ A \in V \to ⦋ A / x ⦌ y = y$
38	37	opeq2d	$⊢ A \in V \to ⟨⦋ A / x ⦌ N, ⦋ A / x ⦌ y⟩ = ⟨⦋ A / x ⦌ N, y⟩$
39	36 38	eqtrd	$⊢ A \in V \to ⦋ A / x ⦌ ⟨N, y⟩ = ⟨⦋ A / x ⦌ N, y⟩$
40		rdgeq12	$⊢ (⦋ A / x ⦌ (n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in U), \emptyset, if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))) = (n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in ⦋ A / x ⦌ U), \emptyset, if (z \in (V \times ⦋ A / x ⦌ U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))) \land ⦋ A / x ⦌ ⟨N, y⟩ = ⟨⦋ A / x ⦌ N, y⟩) \to rec (⦋ A / x ⦌ (n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in U), \emptyset, if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⦋ A / x ⦌ ⟨N, y⟩) = rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in ⦋ A / x ⦌ U), \emptyset, if (z \in (V \times ⦋ A / x ⦌ U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨⦋ A / x ⦌ N, y⟩)$
41	35 39 40	syl2anc	$⊢ A \in V \to rec (⦋ A / x ⦌ (n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in U), \emptyset, if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⦋ A / x ⦌ ⟨N, y⟩) = rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in ⦋ A / x ⦌ U), \emptyset, if (z \in (V \times ⦋ A / x ⦌ U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨⦋ A / x ⦌ N, y⟩)$
42	7 41	eqtrd	$⊢ A \in V \to ⦋ A / x ⦌ rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in U), \emptyset, if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨N, y⟩) = rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in ⦋ A / x ⦌ U), \emptyset, if (z \in (V \times ⦋ A / x ⦌ U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨⦋ A / x ⦌ N, y⟩)$
43	42	fveq1d	$⊢ A \in V \to ⦋ A / x ⦌ rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in U), \emptyset, if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨N, y⟩) (⦋ A / x ⦌ N) = rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in ⦋ A / x ⦌ U), \emptyset, if (z \in (V \times ⦋ A / x ⦌ U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨⦋ A / x ⦌ N, y⟩) (⦋ A / x ⦌ N)$
44	6 43	syl5eq	$⊢ A \in V \to ⦋ A / x ⦌ rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in U), \emptyset, if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨N, y⟩) (N) = rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in ⦋ A / x ⦌ U), \emptyset, if (z \in (V \times ⦋ A / x ⦌ U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨⦋ A / x ⦌ N, y⟩) (⦋ A / x ⦌ N)$
45	44	eqeq2d	$⊢ A \in V \to (\emptyset = ⦋ A / x ⦌ rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in U), \emptyset, if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨N, y⟩) (N) \leftrightarrow \emptyset = rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in ⦋ A / x ⦌ U), \emptyset, if (z \in (V \times ⦋ A / x ⦌ U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨⦋ A / x ⦌ N, y⟩) (⦋ A / x ⦌ N))$
46	5 45	bitrd	$⊢ A \in V \to (\underset{˙}{[} A / x \underset{˙}{]} \emptyset = rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in U), \emptyset, if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨N, y⟩) (N) \leftrightarrow \emptyset = rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in ⦋ A / x ⦌ U), \emptyset, if (z \in (V \times ⦋ A / x ⦌ U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨⦋ A / x ⦌ N, y⟩) (⦋ A / x ⦌ N))$
47	4 46	anbi12d	$⊢ A \in V \to ((\underset{˙}{[} A / x \underset{˙}{]} N \in ω \land \underset{˙}{[} A / x \underset{˙}{]} \emptyset = rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in U), \emptyset, if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨N, y⟩) (N)) \leftrightarrow (⦋ A / x ⦌ N \in ω \land \emptyset = rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in ⦋ A / x ⦌ U), \emptyset, if (z \in (V \times ⦋ A / x ⦌ U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨⦋ A / x ⦌ N, y⟩) (⦋ A / x ⦌ N)))$
48	3 47	syl5bb	$⊢ A \in V \to (\underset{˙}{[} A / x \underset{˙}{]} (N \in ω \land \emptyset = rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in U), \emptyset, if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨N, y⟩) (N)) \leftrightarrow (⦋ A / x ⦌ N \in ω \land \emptyset = rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in ⦋ A / x ⦌ U), \emptyset, if (z \in (V \times ⦋ A / x ⦌ U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨⦋ A / x ⦌ N, y⟩) (⦋ A / x ⦌ N)))$
49	48	abbidv	$⊢ A \in V \to \{y \| \underset{˙}{[} A / x \underset{˙}{]} (N \in ω \land \emptyset = rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in U), \emptyset, if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨N, y⟩) (N))\} = \{y \| (⦋ A / x ⦌ N \in ω \land \emptyset = rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in ⦋ A / x ⦌ U), \emptyset, if (z \in (V \times ⦋ A / x ⦌ U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨⦋ A / x ⦌ N, y⟩) (⦋ A / x ⦌ N))\}$
50		csbab	$⊢ ⦋ A / x ⦌ \{y \| (N \in ω \land \emptyset = rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in U), \emptyset, if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨N, y⟩) (N))\} = \{y \| \underset{˙}{[} A / x \underset{˙}{]} (N \in ω \land \emptyset = rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in U), \emptyset, if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨N, y⟩) (N))\}$
51		df-finxp	$⊢ ⦋ A / x ⦌ U ↑↑ ⦋ A / x ⦌ N = \{y \| (⦋ A / x ⦌ N \in ω \land \emptyset = rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in ⦋ A / x ⦌ U), \emptyset, if (z \in (V \times ⦋ A / x ⦌ U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨⦋ A / x ⦌ N, y⟩) (⦋ A / x ⦌ N))\}$
52	49 50 51	3eqtr4g	$⊢ A \in V \to ⦋ A / x ⦌ \{y \| (N \in ω \land \emptyset = rec ((n \in ω, z \in V ⟼ if ((n = 1_{𝑜} \land z \in U), \emptyset, if (z \in (V \times U), ⟨⋃ n, 1^{st} (z)⟩, ⟨n, z⟩))), ⟨N, y⟩) (N))\} = ⦋ A / x ⦌ U ↑↑ ⦋ A / x ⦌ N$
53	2 52	syl5eq	$⊢ A \in V \to ⦋ A / x ⦌ U ↑↑ N = ⦋ A / x ⦌ U ↑↑ ⦋ A / x ⦌ N$

Metamath Proof Explorer

Theorem csbfinxpg

Proof