relexpsucnnr

Description: A reduction for relation exponentiation to the right. (Contributed by RP, 22-May-2020)

		Ref	Expression
	Assertion	relexpsucnnr	$⊢ (R \in V \land N \in ℕ) \to R ↑_{r} (N + 1) = (R ↑_{r} N) \circ R$

Proof

Step	Hyp	Ref	Expression
1		eqidd	$⊢ (R \in V \land N \in ℕ) \to (r \in V, n \in ℕ_{0} ⟼ if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n))) = (r \in V, n \in ℕ_{0} ⟼ if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n)))$
2		simprr	$⊢ ((R \in V \land N \in ℕ) \land (r = R \land n = N + 1)) \to n = N + 1$
3		dmeq	$⊢ r = R \to dom r = dom R$
4		rneq	$⊢ r = R \to ran r = ran R$
5	3 4	uneq12d	$⊢ r = R \to dom r \cup ran r = dom R \cup ran R$
6	5	reseq2d	$⊢ r = R \to {I ↾}_{(dom r \cup ran r)} = {I ↾}_{(dom R \cup ran R)}$
7		eqidd	$⊢ r = R \to 1 = 1$
8		coeq2	$⊢ r = R \to x \circ r = x \circ R$
9	8	mpoeq3dv	$⊢ r = R \to (x \in V, y \in V ⟼ x \circ r) = (x \in V, y \in V ⟼ x \circ R)$
10		id	$⊢ r = R \to r = R$
11	10	mpteq2dv	$⊢ r = R \to (z \in V ⟼ r) = (z \in V ⟼ R)$
12	7 9 11	seqeq123d	$⊢ r = R \to seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) = seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R))$
13	12	fveq1d	$⊢ r = R \to seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (N + 1) = seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N + 1)$
14	6 13	ifeq12d	$⊢ r = R \to if (N + 1 = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (N + 1)) = if (N + 1 = 0, {I ↾}_{(dom R \cup ran R)}, seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N + 1))$
15	14	ad2antrl	$⊢ ((R \in V \land N \in ℕ) \land (r = R \land N + 1 = N + 1)) \to if (N + 1 = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (N + 1)) = if (N + 1 = 0, {I ↾}_{(dom R \cup ran R)}, seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N + 1))$
16	15	a1i	$⊢ n = N + 1 \to (((R \in V \land N \in ℕ) \land (r = R \land N + 1 = N + 1)) \to if (N + 1 = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (N + 1)) = if (N + 1 = 0, {I ↾}_{(dom R \cup ran R)}, seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N + 1)))$
17		eqeq1	$⊢ n = N + 1 \to (n = N + 1 \leftrightarrow N + 1 = N + 1)$
18	17	anbi2d	$⊢ n = N + 1 \to ((r = R \land n = N + 1) \leftrightarrow (r = R \land N + 1 = N + 1))$
19	18	anbi2d	$⊢ n = N + 1 \to (((R \in V \land N \in ℕ) \land (r = R \land n = N + 1)) \leftrightarrow ((R \in V \land N \in ℕ) \land (r = R \land N + 1 = N + 1)))$
20		eqeq1	$⊢ n = N + 1 \to (n = 0 \leftrightarrow N + 1 = 0)$
21		fveq2	$⊢ n = N + 1 \to seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n) = seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (N + 1)$
22	20 21	ifbieq2d	$⊢ n = N + 1 \to if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n)) = if (N + 1 = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (N + 1))$
23	22	eqeq1d	$⊢ n = N + 1 \to (if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n)) = if (N + 1 = 0, {I ↾}_{(dom R \cup ran R)}, seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N + 1)) \leftrightarrow if (N + 1 = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (N + 1)) = if (N + 1 = 0, {I ↾}_{(dom R \cup ran R)}, seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N + 1)))$
24	16 19 23	3imtr4d	$⊢ n = N + 1 \to (((R \in V \land N \in ℕ) \land (r = R \land n = N + 1)) \to if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n)) = if (N + 1 = 0, {I ↾}_{(dom R \cup ran R)}, seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N + 1)))$
25	2 24	mpcom	$⊢ ((R \in V \land N \in ℕ) \land (r = R \land n = N + 1)) \to if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n)) = if (N + 1 = 0, {I ↾}_{(dom R \cup ran R)}, seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N + 1))$
26		elex	$⊢ R \in V \to R \in V$
27	26	adantr	$⊢ (R \in V \land N \in ℕ) \to R \in V$
28		simpr	$⊢ (R \in V \land N \in ℕ) \to N \in ℕ$
29	28	peano2nnd	$⊢ (R \in V \land N \in ℕ) \to N + 1 \in ℕ$
30	29	nnnn0d	$⊢ (R \in V \land N \in ℕ) \to N + 1 \in ℕ_{0}$
31		dmexg	$⊢ R \in V \to dom R \in V$
32		rnexg	$⊢ R \in V \to ran R \in V$
33		unexg	$⊢ (dom R \in V \land ran R \in V) \to dom R \cup ran R \in V$
34	31 32 33	syl2anc	$⊢ R \in V \to dom R \cup ran R \in V$
35		resiexg	$⊢ dom R \cup ran R \in V \to {I ↾}_{(dom R \cup ran R)} \in V$
36	34 35	syl	$⊢ R \in V \to {I ↾}_{(dom R \cup ran R)} \in V$
37	36	adantr	$⊢ (R \in V \land N \in ℕ) \to {I ↾}_{(dom R \cup ran R)} \in V$
38		fvexd	$⊢ (R \in V \land N \in ℕ) \to seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N + 1) \in V$
39	37 38	ifcld	$⊢ (R \in V \land N \in ℕ) \to if (N + 1 = 0, {I ↾}_{(dom R \cup ran R)}, seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N + 1)) \in V$
40	1 25 27 30 39	ovmpod	$⊢ (R \in V \land N \in ℕ) \to R (r \in V, n \in ℕ_{0} ⟼ if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n))) (N + 1) = if (N + 1 = 0, {I ↾}_{(dom R \cup ran R)}, seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N + 1))$
41		nnne0	$⊢ N + 1 \in ℕ \to N + 1 \neq 0$
42	41	neneqd	$⊢ N + 1 \in ℕ \to \neg N + 1 = 0$
43	29 42	syl	$⊢ (R \in V \land N \in ℕ) \to \neg N + 1 = 0$
44	43	iffalsed	$⊢ (R \in V \land N \in ℕ) \to if (N + 1 = 0, {I ↾}_{(dom R \cup ran R)}, seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N + 1)) = seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N + 1)$
45		elnnuz	$⊢ N \in ℕ \leftrightarrow N \in ℤ_{\geq 1}$
46	45	bilani	$⊢ (R \in V \land N \in ℕ) \to N \in ℤ_{\geq 1}$
47		seqp1	$⊢ N \in ℤ_{\geq 1} \to seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N + 1) = seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N) (x \in V, y \in V ⟼ x \circ R) (z \in V ⟼ R) (N + 1)$
48	46 47	syl	$⊢ (R \in V \land N \in ℕ) \to seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N + 1) = seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N) (x \in V, y \in V ⟼ x \circ R) (z \in V ⟼ R) (N + 1)$
49		ovex	$⊢ N + 1 \in V$
50		simpl	$⊢ (R \in V \land N \in ℕ) \to R \in V$
51		eqidd	$⊢ z = N + 1 \to R = R$
52		eqid	$⊢ (z \in V ⟼ R) = (z \in V ⟼ R)$
53	51 52	fvmptg	$⊢ (N + 1 \in V \land R \in V) \to (z \in V ⟼ R) (N + 1) = R$
54	49 50 53	sylancr	$⊢ (R \in V \land N \in ℕ) \to (z \in V ⟼ R) (N + 1) = R$
55	54	oveq2d	$⊢ (R \in V \land N \in ℕ) \to seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N) (x \in V, y \in V ⟼ x \circ R) (z \in V ⟼ R) (N + 1) = seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N) (x \in V, y \in V ⟼ x \circ R) R$
56		nfcv	$⊢ \underline{Ⅎ} a (x \circ R)$
57		nfcv	$⊢ \underline{Ⅎ} b (x \circ R)$
58		nfcv	$⊢ \underline{Ⅎ} x (a \circ R)$
59		nfcv	$⊢ \underline{Ⅎ} y (a \circ R)$
60		simpl	$⊢ (x = a \land y = b) \to x = a$
61	60	coeq1d	$⊢ (x = a \land y = b) \to x \circ R = a \circ R$
62	56 57 58 59 61	cbvmpo	$⊢ (x \in V, y \in V ⟼ x \circ R) = (a \in V, b \in V ⟼ a \circ R)$
63		oveq	$⊢ (x \in V, y \in V ⟼ x \circ R) = (a \in V, b \in V ⟼ a \circ R) \to seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N) (x \in V, y \in V ⟼ x \circ R) R = seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N) (a \in V, b \in V ⟼ a \circ R) R$
64	62 63	mp1i	$⊢ (R \in V \land N \in ℕ) \to seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N) (x \in V, y \in V ⟼ x \circ R) R = seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N) (a \in V, b \in V ⟼ a \circ R) R$
65		eqidd	$⊢ (R \in V \land N \in ℕ) \to (a \in V, b \in V ⟼ a \circ R) = (a \in V, b \in V ⟼ a \circ R)$
66		simprl	$⊢ ((R \in V \land N \in ℕ) \land (a = seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N) \land b = R)) \to a = seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N)$
67	66	coeq1d	$⊢ ((R \in V \land N \in ℕ) \land (a = seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N) \land b = R)) \to a \circ R = seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N) \circ R$
68		fvexd	$⊢ (R \in V \land N \in ℕ) \to seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N) \in V$
69		fvex	$⊢ seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N) \in V$
70		coexg	$⊢ (seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N) \in V \land R \in V) \to seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N) \circ R \in V$
71	69 50 70	sylancr	$⊢ (R \in V \land N \in ℕ) \to seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N) \circ R \in V$
72	65 67 68 27 71	ovmpod	$⊢ (R \in V \land N \in ℕ) \to seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N) (a \in V, b \in V ⟼ a \circ R) R = seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N) \circ R$
73		simpr	$⊢ (r = R \land n = N) \to n = N$
74	73	eqeq1d	$⊢ (r = R \land n = N) \to (n = 0 \leftrightarrow N = 0)$
75	6	adantr	$⊢ (r = R \land n = N) \to {I ↾}_{(dom r \cup ran r)} = {I ↾}_{(dom R \cup ran R)}$
76	12	adantr	$⊢ (r = R \land n = N) \to seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) = seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R))$
77	76 73	fveq12d	$⊢ (r = R \land n = N) \to seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n) = seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N)$
78	74 75 77	ifbieq12d	$⊢ (r = R \land n = N) \to if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n)) = if (N = 0, {I ↾}_{(dom R \cup ran R)}, seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N))$
79	78	adantl	$⊢ ((R \in V \land N \in ℕ) \land (r = R \land n = N)) \to if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n)) = if (N = 0, {I ↾}_{(dom R \cup ran R)}, seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N))$
80	28	nnnn0d	$⊢ (R \in V \land N \in ℕ) \to N \in ℕ_{0}$
81	37 68	ifcld	$⊢ (R \in V \land N \in ℕ) \to if (N = 0, {I ↾}_{(dom R \cup ran R)}, seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N)) \in V$
82	1 79 27 80 81	ovmpod	$⊢ (R \in V \land N \in ℕ) \to R (r \in V, n \in ℕ_{0} ⟼ if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n))) N = if (N = 0, {I ↾}_{(dom R \cup ran R)}, seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N))$
83		nnne0	$⊢ N \in ℕ \to N \neq 0$
84	83	adantl	$⊢ (R \in V \land N \in ℕ) \to N \neq 0$
85	84	neneqd	$⊢ (R \in V \land N \in ℕ) \to \neg N = 0$
86	85	iffalsed	$⊢ (R \in V \land N \in ℕ) \to if (N = 0, {I ↾}_{(dom R \cup ran R)}, seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N)) = seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N)$
87	82 86	eqtr2d	$⊢ (R \in V \land N \in ℕ) \to seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N) = R (r \in V, n \in ℕ_{0} ⟼ if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n))) N$
88	87	coeq1d	$⊢ (R \in V \land N \in ℕ) \to seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N) \circ R = (R (r \in V, n \in ℕ_{0} ⟼ if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n))) N) \circ R$
89	64 72 88	3eqtrd	$⊢ (R \in V \land N \in ℕ) \to seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N) (x \in V, y \in V ⟼ x \circ R) R = (R (r \in V, n \in ℕ_{0} ⟼ if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n))) N) \circ R$
90	48 55 89	3eqtrd	$⊢ (R \in V \land N \in ℕ) \to seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N + 1) = (R (r \in V, n \in ℕ_{0} ⟼ if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n))) N) \circ R$
91	40 44 90	3eqtrd	$⊢ (R \in V \land N \in ℕ) \to R (r \in V, n \in ℕ_{0} ⟼ if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n))) (N + 1) = (R (r \in V, n \in ℕ_{0} ⟼ if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n))) N) \circ R$
92		df-relexp	$⊢ ↑_{r} = (r \in V, n \in ℕ_{0} ⟼ if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n)))$
93		oveq	$⊢ ↑_{r} = (r \in V, n \in ℕ_{0} ⟼ if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n))) \to R ↑_{r} (N + 1) = R (r \in V, n \in ℕ_{0} ⟼ if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n))) (N + 1)$
94		oveq	$⊢ ↑_{r} = (r \in V, n \in ℕ_{0} ⟼ if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n))) \to R ↑_{r} N = R (r \in V, n \in ℕ_{0} ⟼ if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n))) N$
95	94	coeq1d	$⊢ ↑_{r} = (r \in V, n \in ℕ_{0} ⟼ if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n))) \to (R ↑_{r} N) \circ R = (R (r \in V, n \in ℕ_{0} ⟼ if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n))) N) \circ R$
96	93 95	eqeq12d	$⊢ ↑_{r} = (r \in V, n \in ℕ_{0} ⟼ if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n))) \to (R ↑_{r} (N + 1) = (R ↑_{r} N) \circ R \leftrightarrow R (r \in V, n \in ℕ_{0} ⟼ if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n))) (N + 1) = (R (r \in V, n \in ℕ_{0} ⟼ if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n))) N) \circ R)$
97	96	imbi2d	$⊢ ↑_{r} = (r \in V, n \in ℕ_{0} ⟼ if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n))) \to (((R \in V \land N \in ℕ) \to R ↑_{r} (N + 1) = (R ↑_{r} N) \circ R) \leftrightarrow ((R \in V \land N \in ℕ) \to R (r \in V, n \in ℕ_{0} ⟼ if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n))) (N + 1) = (R (r \in V, n \in ℕ_{0} ⟼ if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n))) N) \circ R))$
98	92 97	ax-mp	$⊢ ((R \in V \land N \in ℕ) \to R ↑_{r} (N + 1) = (R ↑_{r} N) \circ R) \leftrightarrow ((R \in V \land N \in ℕ) \to R (r \in V, n \in ℕ_{0} ⟼ if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n))) (N + 1) = (R (r \in V, n \in ℕ_{0} ⟼ if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n))) N) \circ R)$
99	91 98	mpbir	$⊢ (R \in V \land N \in ℕ) \to R ↑_{r} (N + 1) = (R ↑_{r} N) \circ R$

Metamath Proof Explorer

Theorem relexpsucnnr

Proof