relexpuzrel

Description: The exponentiation of a class to an integer not smaller than 2 is a relation. (Contributed by RP, 23-May-2020)

		Ref	Expression
	Assertion	relexpuzrel	$⊢ (N \in ℤ_{\geq 2} \land R \in V) \to Rel (R ↑_{r} N)$

Step	Hyp	Ref	Expression
1		eluzge2nn0	$⊢ N \in ℤ_{\geq 2} \to N \in ℕ_{0}$
2	1	adantr	$⊢ (N \in ℤ_{\geq 2} \land R \in V) \to N \in ℕ_{0}$
3		simpr	$⊢ (N \in ℤ_{\geq 2} \land R \in V) \to R \in V$
4		eluz2b3	$⊢ N \in ℤ_{\geq 2} \leftrightarrow (N \in ℕ \land N \neq 1)$
5	4	simprbi	$⊢ N \in ℤ_{\geq 2} \to N \neq 1$
6	5	adantr	$⊢ (N \in ℤ_{\geq 2} \land R \in V) \to N \neq 1$
7	6	neneqd	$⊢ (N \in ℤ_{\geq 2} \land R \in V) \to \neg N = 1$
8	7	pm2.21d	$⊢ (N \in ℤ_{\geq 2} \land R \in V) \to (N = 1 \to Rel R)$
9		relexprelg	$⊢ (N \in ℕ_{0} \land R \in V \land (N = 1 \to Rel R)) \to Rel (R ↑_{r} N)$
10	2 3 8 9	syl3anc	$⊢ (N \in ℤ_{\geq 2} \land R \in V) \to Rel (R ↑_{r} N)$

Metamath Proof Explorer