finxpsuc

Description: The value of Cartesian exponentiation at a successor. (Contributed by ML, 24-Oct-2020)

		Ref	Expression
	Assertion	finxpsuc	$⊢ (N \in ω \land N \neq \emptyset) \to U ↑↑ suc N = U ↑↑ N \times U$

Step	Hyp	Ref	Expression
1		nnord	$⊢ N \in ω \to Ord N$
2		ordge1n0	$⊢ Ord N \to (1_{𝑜} \subseteq N \leftrightarrow N \neq \emptyset)$
3	1 2	syl	$⊢ N \in ω \to (1_{𝑜} \subseteq N \leftrightarrow N \neq \emptyset)$
4	3	biimprd	$⊢ N \in ω \to (N \neq \emptyset \to 1_{𝑜} \subseteq N)$
5	4	imdistani	$⊢ (N \in ω \land N \neq \emptyset) \to (N \in ω \land 1_{𝑜} \subseteq N)$
6		eqid	$⊢ (y \in ω, x \in V ⟼ if ((y = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ y, 1^{st} (x)⟩, ⟨y, x⟩))) = (y \in ω, x \in V ⟼ if ((y = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ y, 1^{st} (x)⟩, ⟨y, x⟩)))$
7	6	finxpsuclem	$⊢ (N \in ω \land 1_{𝑜} \subseteq N) \to U ↑↑ suc N = U ↑↑ N \times U$
8	5 7	syl	$⊢ (N \in ω \land N \neq \emptyset) \to U ↑↑ suc N = U ↑↑ N \times U$

Metamath Proof Explorer