relexprelg

Description: The exponentiation of a class is a relation except when the exponent is one and the class is not a relation. (Contributed by RP, 23-May-2020)

		Ref	Expression
	Assertion	relexprelg	$⊢ (N \in ℕ_{0} \land R \in V \land (N = 1 \to Rel R)) \to Rel (R ↑_{r} N)$

Proof

Step	Hyp	Ref	Expression
1		elnn0	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℕ \lor N = 0)$
2		eqeq1	$⊢ n = 1 \to (n = 1 \leftrightarrow 1 = 1)$
3	2	imbi1d	$⊢ n = 1 \to ((n = 1 \to Rel R) \leftrightarrow (1 = 1 \to Rel R))$
4	3	anbi2d	$⊢ n = 1 \to ((R \in V \land (n = 1 \to Rel R)) \leftrightarrow (R \in V \land (1 = 1 \to Rel R)))$
5		oveq2	$⊢ n = 1 \to R ↑_{r} n = R ↑_{r} 1$
6	5	releqd	$⊢ n = 1 \to (Rel (R ↑_{r} n) \leftrightarrow Rel (R ↑_{r} 1))$
7	4 6	imbi12d	$⊢ n = 1 \to (((R \in V \land (n = 1 \to Rel R)) \to Rel (R ↑_{r} n)) \leftrightarrow ((R \in V \land (1 = 1 \to Rel R)) \to Rel (R ↑_{r} 1)))$
8		eqeq1	$⊢ n = m \to (n = 1 \leftrightarrow m = 1)$
9	8	imbi1d	$⊢ n = m \to ((n = 1 \to Rel R) \leftrightarrow (m = 1 \to Rel R))$
10	9	anbi2d	$⊢ n = m \to ((R \in V \land (n = 1 \to Rel R)) \leftrightarrow (R \in V \land (m = 1 \to Rel R)))$
11		oveq2	$⊢ n = m \to R ↑_{r} n = R ↑_{r} m$
12	11	releqd	$⊢ n = m \to (Rel (R ↑_{r} n) \leftrightarrow Rel (R ↑_{r} m))$
13	10 12	imbi12d	$⊢ n = m \to (((R \in V \land (n = 1 \to Rel R)) \to Rel (R ↑_{r} n)) \leftrightarrow ((R \in V \land (m = 1 \to Rel R)) \to Rel (R ↑_{r} m)))$
14		eqeq1	$⊢ n = m + 1 \to (n = 1 \leftrightarrow m + 1 = 1)$
15	14	imbi1d	$⊢ n = m + 1 \to ((n = 1 \to Rel R) \leftrightarrow (m + 1 = 1 \to Rel R))$
16	15	anbi2d	$⊢ n = m + 1 \to ((R \in V \land (n = 1 \to Rel R)) \leftrightarrow (R \in V \land (m + 1 = 1 \to Rel R)))$
17		oveq2	$⊢ n = m + 1 \to R ↑_{r} n = R ↑_{r} (m + 1)$
18	17	releqd	$⊢ n = m + 1 \to (Rel (R ↑_{r} n) \leftrightarrow Rel (R ↑_{r} (m + 1)))$
19	16 18	imbi12d	$⊢ n = m + 1 \to (((R \in V \land (n = 1 \to Rel R)) \to Rel (R ↑_{r} n)) \leftrightarrow ((R \in V \land (m + 1 = 1 \to Rel R)) \to Rel (R ↑_{r} (m + 1))))$
20		eqeq1	$⊢ n = N \to (n = 1 \leftrightarrow N = 1)$
21	20	imbi1d	$⊢ n = N \to ((n = 1 \to Rel R) \leftrightarrow (N = 1 \to Rel R))$
22	21	anbi2d	$⊢ n = N \to ((R \in V \land (n = 1 \to Rel R)) \leftrightarrow (R \in V \land (N = 1 \to Rel R)))$
23		oveq2	$⊢ n = N \to R ↑_{r} n = R ↑_{r} N$
24	23	releqd	$⊢ n = N \to (Rel (R ↑_{r} n) \leftrightarrow Rel (R ↑_{r} N))$
25	22 24	imbi12d	$⊢ n = N \to (((R \in V \land (n = 1 \to Rel R)) \to Rel (R ↑_{r} n)) \leftrightarrow ((R \in V \land (N = 1 \to Rel R)) \to Rel (R ↑_{r} N)))$
26		eqid	$⊢ 1 = 1$
27		pm2.27	$⊢ 1 = 1 \to ((1 = 1 \to Rel R) \to Rel R)$
28	26 27	ax-mp	$⊢ (1 = 1 \to Rel R) \to Rel R$
29	28	adantl	$⊢ (R \in V \land (1 = 1 \to Rel R)) \to Rel R$
30		relexp1g	$⊢ R \in V \to R ↑_{r} 1 = R$
31	30	adantr	$⊢ (R \in V \land (1 = 1 \to Rel R)) \to R ↑_{r} 1 = R$
32	31	releqd	$⊢ (R \in V \land (1 = 1 \to Rel R)) \to (Rel (R ↑_{r} 1) \leftrightarrow Rel R)$
33	29 32	mpbird	$⊢ (R \in V \land (1 = 1 \to Rel R)) \to Rel (R ↑_{r} 1)$
34		relco	$⊢ Rel ((R ↑_{r} m) \circ R)$
35		relexpsucnnr	$⊢ (R \in V \land m \in ℕ) \to R ↑_{r} (m + 1) = (R ↑_{r} m) \circ R$
36	35	ancoms	$⊢ (m \in ℕ \land R \in V) \to R ↑_{r} (m + 1) = (R ↑_{r} m) \circ R$
37	36	releqd	$⊢ (m \in ℕ \land R \in V) \to (Rel (R ↑_{r} (m + 1)) \leftrightarrow Rel ((R ↑_{r} m) \circ R))$
38	34 37	mpbiri	$⊢ (m \in ℕ \land R \in V) \to Rel (R ↑_{r} (m + 1))$
39	38	a1d	$⊢ (m \in ℕ \land R \in V) \to ((m + 1 = 1 \to Rel R) \to Rel (R ↑_{r} (m + 1)))$
40	39	expimpd	$⊢ m \in ℕ \to ((R \in V \land (m + 1 = 1 \to Rel R)) \to Rel (R ↑_{r} (m + 1)))$
41	40	a1d	$⊢ m \in ℕ \to (((R \in V \land (m = 1 \to Rel R)) \to Rel (R ↑_{r} m)) \to ((R \in V \land (m + 1 = 1 \to Rel R)) \to Rel (R ↑_{r} (m + 1))))$
42	7 13 19 25 33 41	nnind	$⊢ N \in ℕ \to ((R \in V \land (N = 1 \to Rel R)) \to Rel (R ↑_{r} N))$
43		relexp0rel	$⊢ R \in V \to Rel (R ↑_{r} 0)$
44	43	adantl	$⊢ (N = 0 \land R \in V) \to Rel (R ↑_{r} 0)$
45		simpl	$⊢ (N = 0 \land R \in V) \to N = 0$
46	45	oveq2d	$⊢ (N = 0 \land R \in V) \to R ↑_{r} N = R ↑_{r} 0$
47	46	releqd	$⊢ (N = 0 \land R \in V) \to (Rel (R ↑_{r} N) \leftrightarrow Rel (R ↑_{r} 0))$
48	44 47	mpbird	$⊢ (N = 0 \land R \in V) \to Rel (R ↑_{r} N)$
49	48	a1d	$⊢ (N = 0 \land R \in V) \to ((N = 1 \to Rel R) \to Rel (R ↑_{r} N))$
50	49	expimpd	$⊢ N = 0 \to ((R \in V \land (N = 1 \to Rel R)) \to Rel (R ↑_{r} N))$
51	42 50	jaoi	$⊢ (N \in ℕ \lor N = 0) \to ((R \in V \land (N = 1 \to Rel R)) \to Rel (R ↑_{r} N))$
52	1 51	sylbi	$⊢ N \in ℕ_{0} \to ((R \in V \land (N = 1 \to Rel R)) \to Rel (R ↑_{r} N))$
53	52	3impib	$⊢ (N \in ℕ_{0} \land R \in V \land (N = 1 \to Rel R)) \to Rel (R ↑_{r} N)$

Metamath Proof Explorer

Theorem relexprelg

Proof