Metamath Proof Explorer

Theorem finxpeq2

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

		Ref	Expression
	Assertion	finxpeq2	$⊢ M = N \to U ↑↑ M = U ↑↑ N$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$⊢ M = N \to (M \in ω \leftrightarrow N \in ω)$
2		opeq1	$⊢ M = N \to ⟨M, y⟩ = ⟨N, y⟩$
3		rdgeq2	$⊢ ⟨M, y⟩ = ⟨N, y⟩ \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⟩))), ⟨M, y⟩) = 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⟩)$
4	2 3	syl	$⊢ M = N \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⟩))), ⟨M, y⟩) = 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⟩)$
5		id	$⊢ M = N \to M = N$
6	4 5	fveq12d	$⊢ M = N \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⟩))), ⟨M, y⟩) (M) = 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)$
7	6	eqeq2d	$⊢ M = N \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⟩))), ⟨M, y⟩) (M) \leftrightarrow \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))$
8	1 7	anbi12d	$⊢ M = N \to ((M \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⟩))), ⟨M, y⟩) (M)) \leftrightarrow (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)))$
9	8	abbidv	$⊢ M = N \to \{y \| (M \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⟩))), ⟨M, y⟩) (M))\} = \{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))\}$
10		df-finxp	$⊢ U ↑↑ M = \{y \| (M \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⟩))), ⟨M, y⟩) (M))\}$
11		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))\}$
12	9 10 11	3eqtr4g	$⊢ M = N \to U ↑↑ M = U ↑↑ N$