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	biimpi	$⊢ N \in ℕ \to N \in ℤ_{\geq 1}$
47	46	adantl	$⊢ (R \in V \land N \in ℕ) \to N \in ℤ_{\geq 1}$
48		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)$
49	47 48	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)$
50		ovex	$⊢ N + 1 \in V$
51		simpl	$⊢ (R \in V \land N \in ℕ) \to R \in V$
52		eqidd	$⊢ z = N + 1 \to R = R$
53		eqid	$⊢ (z \in V ⟼ R) = (z \in V ⟼ R)$
54	52 53	fvmptg	$⊢ (N + 1 \in V \land R \in V) \to (z \in V ⟼ R) (N + 1) = R$
55	50 51 54	sylancr	$⊢ (R \in V \land N \in ℕ) \to (z \in V ⟼ R) (N + 1) = R$
56	55	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$
57		nfcv	$⊢ \underline{Ⅎ} a (x \circ R)$
58		nfcv	$⊢ \underline{Ⅎ} b (x \circ R)$
59		nfcv	$⊢ \underline{Ⅎ} x (a \circ R)$
60		nfcv	$⊢ \underline{Ⅎ} y (a \circ R)$
61		simpl	$⊢ (x = a \land y = b) \to x = a$
62	61	coeq1d	$⊢ (x = a \land y = b) \to x \circ R = a \circ R$
63	57 58 59 60 62	cbvmpo	$⊢ (x \in V, y \in V ⟼ x \circ R) = (a \in V, b \in V ⟼ a \circ R)$
64		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$
65	63 64	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$
66		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)$
67		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)$
68	67	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$
69		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$
70		fvex	$⊢ seq 1 ((x \in V, y \in V ⟼ x \circ R), (z \in V ⟼ R)) (N) \in V$
71		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$
72	70 51 71	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$
73	66 68 69 27 72	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$
74		simpr	$⊢ (r = R \land n = N) \to n = N$
75	74	eqeq1d	$⊢ (r = R \land n = N) \to (n = 0 \leftrightarrow N = 0)$
76	6	adantr	$⊢ (r = R \land n = N) \to {I ↾}_{(dom r \cup ran r)} = {I ↾}_{(dom R \cup ran R)}$
77	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))$
78	77 74	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)$
79	75 76 78	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))$
80	79	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))$
81	28	nnnn0d	$⊢ (R \in V \land N \in ℕ) \to N \in ℕ_{0}$
82	37 69	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$
83	1 80 27 81 82	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))$
84		nnne0	$⊢ N \in ℕ \to N \neq 0$
85	84	adantl	$⊢ (R \in V \land N \in ℕ) \to N \neq 0$
86	85	neneqd	$⊢ (R \in V \land N \in ℕ) \to \neg N = 0$
87	86	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)$
88	83 87	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$
89	88	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$
90	65 73 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) (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$
91	49 56 90	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$
92	40 44 91	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$
93		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)))$
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 + 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)$
95		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$
96	95	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$
97	94 96	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)$
98	97	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))$
99	93 98	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)$
100	92 99	mpbir	$⊢ (R \in V \land N \in ℕ) \to R ↑_{r} (N + 1) = (R ↑_{r} N) \circ R$

Metamath Proof Explorer

Theorem relexpsucnnr

Proof