relexp1g

Description: A relation composed once is itself. (Contributed by RP, 22-May-2020)

		Ref	Expression
	Assertion	relexp1g	$⊢ R \in V \to R ↑_{r} 1 = R$

Proof

Step	Hyp	Ref	Expression
1		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)))$
2	1	a1i	$⊢ R \in V \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)))$
3		simprr	$⊢ (R \in V \land (r = R \land n = 1)) \to n = 1$
4		ax-1ne0	$⊢ 1 \neq 0$
5		neeq1	$⊢ n = 1 \to (n \neq 0 \leftrightarrow 1 \neq 0)$
6	4 5	mpbiri	$⊢ n = 1 \to n \neq 0$
7	3 6	syl	$⊢ (R \in V \land (r = R \land n = 1)) \to n \neq 0$
8	7	neneqd	$⊢ (R \in V \land (r = R \land n = 1)) \to \neg n = 0$
9	8	iffalsed	$⊢ (R \in V \land (r = R \land 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)) = seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n)$
10		simprl	$⊢ (R \in V \land (r = R \land n = 1)) \to r = R$
11	10	mpteq2dv	$⊢ (R \in V \land (r = R \land n = 1)) \to (z \in V ⟼ r) = (z \in V ⟼ R)$
12	11	seqeq3d	$⊢ (R \in V \land (r = R \land n = 1)) \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 3	fveq12d	$⊢ (R \in V \land (r = R \land 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)) (1)$
14		1z	$⊢ 1 \in ℤ$
15		eqidd	$⊢ (R \in V \land (r = R \land n = 1)) \to (z \in V ⟼ R) = (z \in V ⟼ R)$
16		eqidd	$⊢ ((R \in V \land (r = R \land n = 1)) \land z = 1) \to R = R$
17		1ex	$⊢ 1 \in V$
18	17	a1i	$⊢ (R \in V \land (r = R \land n = 1)) \to 1 \in V$
19		simpl	$⊢ (R \in V \land (r = R \land n = 1)) \to R \in V$
20	15 16 18 19	fvmptd	$⊢ (R \in V \land (r = R \land n = 1)) \to (z \in V ⟼ R) (1) = R$
21	14 20	seq1i	$⊢ (R \in V \land (r = R \land n = 1)) \to seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ R)) (1) = R$
22	9 13 21	3eqtrd	$⊢ (R \in V \land (r = R \land 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)) = R$
23		elex	$⊢ R \in V \to R \in V$
24		1nn0	$⊢ 1 \in ℕ_{0}$
25	24	a1i	$⊢ R \in V \to 1 \in ℕ_{0}$
26	2 22 23 25 23	ovmpod	$⊢ R \in V \to R ↑_{r} 1 = R$

Metamath Proof Explorer

Theorem relexp1g

Proof