Metamath Proof Explorer

Theorem finxpeq1

Description: Equality theorem for Cartesian exponentiation. (Contributed by ML, 19-Oct-2020)

		Ref	Expression
	Assertion	finxpeq1	$⊢ U = V \to U ↑↑ N = V ↑↑ N$

Proof

Step	Hyp	Ref	Expression
1		eleq2	$⊢ U = V \to (x \in U \leftrightarrow x \in V)$
2	1	anbi2d	$⊢ U = V \to ((n = 1_{𝑜} \land x \in U) \leftrightarrow (n = 1_{𝑜} \land x \in V))$
3		xpeq2	$⊢ U = V \to V \times U = V \times V$
4	3	eleq2d	$⊢ U = V \to (x \in (V \times U) \leftrightarrow x \in (V \times V))$
5	4	ifbid	$⊢ U = V \to if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩) = if (x \in (V \times V), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩)$
6	2 5	ifbieq2d	$⊢ U = V \to if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩)) = if ((n = 1_{𝑜} \land x \in V), \emptyset, if (x \in (V \times V), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))$
7	6	mpoeq3dv	$⊢ U = V \to (n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))) = (n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in V), \emptyset, if (x \in (V \times V), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩)))$
8		rdgeq1	$⊢ (n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))) = (n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in V), \emptyset, if (x \in (V \times V), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))) \to rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨N, y⟩) = rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in V), \emptyset, if (x \in (V \times V), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨N, y⟩)$
9	7 8	syl	$⊢ U = V \to rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨N, y⟩) = rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in V), \emptyset, if (x \in (V \times V), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨N, y⟩)$
10	9	fveq1d	$⊢ U = V \to rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨N, y⟩) (N) = rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in V), \emptyset, if (x \in (V \times V), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨N, y⟩) (N)$
11	10	eqeq2d	$⊢ U = V \to (\emptyset = rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨N, y⟩) (N) \leftrightarrow \emptyset = rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in V), \emptyset, if (x \in (V \times V), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨N, y⟩) (N))$
12	11	anbi2d	$⊢ U = V \to ((N \in ω \land \emptyset = rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨N, y⟩) (N)) \leftrightarrow (N \in ω \land \emptyset = rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in V), \emptyset, if (x \in (V \times V), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨N, y⟩) (N)))$
13	12	abbidv	$⊢ U = V \to \{y \| (N \in ω \land \emptyset = rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨N, y⟩) (N))\} = \{y \| (N \in ω \land \emptyset = rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in V), \emptyset, if (x \in (V \times V), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨N, y⟩) (N))\}$
14		df-finxp	$⊢ U ↑↑ N = \{y \| (N \in ω \land \emptyset = rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨N, y⟩) (N))\}$
15		df-finxp	$⊢ V ↑↑ N = \{y \| (N \in ω \land \emptyset = rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in V), \emptyset, if (x \in (V \times V), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨N, y⟩) (N))\}$
16	13 14 15	3eqtr4g	$⊢ U = V \to U ↑↑ N = V ↑↑ N$