relexp0g

Description: A relation composed zero times is the (restricted) identity. (Contributed by RP, 22-May-2020)

		Ref	Expression
	Assertion	relexp0g	$⊢ R \in V \to R ↑_{r} 0 = {I ↾}_{(dom R \cup ran R)}$

Proof

Step	Hyp	Ref	Expression
1		eqidd	$⊢ R \in V \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 (r = R \land n = 0)) \to n = 0$
3	2	iftrued	$⊢ (R \in V \land (r = R \land n = 0)) \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)) = {I ↾}_{(dom r \cup ran r)}$
4		dmeq	$⊢ r = R \to dom r = dom R$
5		rneq	$⊢ r = R \to ran r = ran R$
6	4 5	uneq12d	$⊢ r = R \to dom r \cup ran r = dom R \cup ran R$
7	6	reseq2d	$⊢ r = R \to {I ↾}_{(dom r \cup ran r)} = {I ↾}_{(dom R \cup ran R)}$
8	7	ad2antrl	$⊢ (R \in V \land (r = R \land n = 0)) \to {I ↾}_{(dom r \cup ran r)} = {I ↾}_{(dom R \cup ran R)}$
9	3 8	eqtrd	$⊢ (R \in V \land (r = R \land n = 0)) \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)) = {I ↾}_{(dom R \cup ran R)}$
10		elex	$⊢ R \in V \to R \in V$
11		0nn0	$⊢ 0 \in ℕ_{0}$
12	11	a1i	$⊢ R \in V \to 0 \in ℕ_{0}$
13		dmexg	$⊢ R \in V \to dom R \in V$
14		rnexg	$⊢ R \in V \to ran R \in V$
15		unexg	$⊢ (dom R \in V \land ran R \in V) \to dom R \cup ran R \in V$
16	13 14 15	syl2anc	$⊢ R \in V \to dom R \cup ran R \in V$
17		resiexg	$⊢ dom R \cup ran R \in V \to {I ↾}_{(dom R \cup ran R)} \in V$
18	16 17	syl	$⊢ R \in V \to {I ↾}_{(dom R \cup ran R)} \in V$
19	1 9 10 12 18	ovmpod	$⊢ 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))) 0 = {I ↾}_{(dom R \cup ran R)}$
20		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)))$
21		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} 0 = 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))) 0$
22	21	eqeq1d	$⊢ ↑_{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} 0 = {I ↾}_{(dom R \cup ran 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))) 0 = {I ↾}_{(dom R \cup ran R)})$
23	22	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 \to R ↑_{r} 0 = {I ↾}_{(dom R \cup ran R)}) \leftrightarrow (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))) 0 = {I ↾}_{(dom R \cup ran R)}))$
24	20 23	ax-mp	$⊢ (R \in V \to R ↑_{r} 0 = {I ↾}_{(dom R \cup ran R)}) \leftrightarrow (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))) 0 = {I ↾}_{(dom R \cup ran R)})$
25	19 24	mpbir	$⊢ R \in V \to R ↑_{r} 0 = {I ↾}_{(dom R \cup ran R)}$

Metamath Proof Explorer

Theorem relexp0g

Proof