Metamath Proof Explorer

Theorem finxpnom

Description: Cartesian exponentiation when the exponent is not a natural number defaults to the empty set. (Contributed by ML, 24-Oct-2020)

		Ref	Expression
	Assertion	finxpnom	$⊢ \neg N \in ω \to U ↑↑ N = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (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)) \to N \in ω$
2	1	con3i	$⊢ \neg N \in ω \to \neg (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))$
3		abid	$⊢ y \in \{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))\} \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))$
4	2 3	sylnibr	$⊢ \neg N \in ω \to \neg y \in \{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))\}$
5		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))\}$
6	5	eleq2i	$⊢ y \in U ↑↑ N \leftrightarrow y \in \{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))\}$
7	4 6	sylnibr	$⊢ \neg N \in ω \to \neg y \in U ↑↑ N$
8	7	eq0rdv	$⊢ \neg N \in ω \to U ↑↑ N = \emptyset$