Metamath Proof Explorer

Theorem finxp0

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

		Ref	Expression
	Assertion	finxp0	$⊢ U ↑↑ \emptyset = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		0ex	$⊢ \emptyset \in V$
2		vex	$⊢ y \in V$
3	1 2	opnzi	$⊢ ⟨\emptyset, y⟩ \neq \emptyset$
4	3	nesymi	$⊢ \neg \emptyset = ⟨\emptyset, y⟩$
5		peano1	$⊢ \emptyset \in ω$
6		df-finxp	$⊢ U ↑↑ \emptyset = \{y \| (\emptyset \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⟩))), ⟨\emptyset, y⟩) (\emptyset))\}$
7	6	eqabri	$⊢ y \in U ↑↑ \emptyset \leftrightarrow (\emptyset \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⟩))), ⟨\emptyset, y⟩) (\emptyset))$
8	5 7	mpbiran	$⊢ y \in U ↑↑ \emptyset \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⟩))), ⟨\emptyset, y⟩) (\emptyset)$
9		opex	$⊢ ⟨\emptyset, y⟩ \in V$
10	9	rdg0	$⊢ 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⟩))), ⟨\emptyset, y⟩) (\emptyset) = ⟨\emptyset, y⟩$
11	10	eqeq2i	$⊢ \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⟩))), ⟨\emptyset, y⟩) (\emptyset) \leftrightarrow \emptyset = ⟨\emptyset, y⟩$
12	8 11	bitri	$⊢ y \in U ↑↑ \emptyset \leftrightarrow \emptyset = ⟨\emptyset, y⟩$
13	4 12	mtbir	$⊢ \neg y \in U ↑↑ \emptyset$
14	13	nel0	$⊢ U ↑↑ \emptyset = \emptyset$