itcoval1

		Ref	Expression
	Assertion	itcoval1	$⊢ (Rel F \land F \in V) \to IterComp (F) (1) = F$

Proof

Step	Hyp	Ref	Expression
1		itcoval	$⊢ F \in V \to IterComp (F) = seq 0 ((g \in V, j \in V ⟼ F \circ g), (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F)))$
2	1	fveq1d	$⊢ F \in V \to IterComp (F) (1) = seq 0 ((g \in V, j \in V ⟼ F \circ g), (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F))) (1)$
3	2	adantl	$⊢ (Rel F \land F \in V) \to IterComp (F) (1) = seq 0 ((g \in V, j \in V ⟼ F \circ g), (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F))) (1)$
4		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
5		0nn0	$⊢ 0 \in ℕ_{0}$
6	5	a1i	$⊢ (Rel F \land F \in V) \to 0 \in ℕ_{0}$
7		1e0p1	$⊢ 1 = 0 + 1$
8	1	eqcomd	$⊢ F \in V \to seq 0 ((g \in V, j \in V ⟼ F \circ g), (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F))) = IterComp (F)$
9	8	fveq1d	$⊢ F \in V \to seq 0 ((g \in V, j \in V ⟼ F \circ g), (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F))) (0) = IterComp (F) (0)$
10		itcoval0	$⊢ F \in V \to IterComp (F) (0) = {I ↾}_{dom F}$
11	9 10	eqtrd	$⊢ F \in V \to seq 0 ((g \in V, j \in V ⟼ F \circ g), (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F))) (0) = {I ↾}_{dom F}$
12	11	adantl	$⊢ (Rel F \land F \in V) \to seq 0 ((g \in V, j \in V ⟼ F \circ g), (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F))) (0) = {I ↾}_{dom F}$
13		eqidd	$⊢ (Rel F \land F \in V) \to (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F)) = (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F))$
14		ax-1ne0	$⊢ 1 \neq 0$
15	14	neii	$⊢ \neg 1 = 0$
16		eqeq1	$⊢ i = 1 \to (i = 0 \leftrightarrow 1 = 0)$
17	15 16	mtbiri	$⊢ i = 1 \to \neg i = 0$
18	17	iffalsed	$⊢ i = 1 \to if (i = 0, {I ↾}_{dom F}, F) = F$
19	18	adantl	$⊢ ((Rel F \land F \in V) \land i = 1) \to if (i = 0, {I ↾}_{dom F}, F) = F$
20		1nn0	$⊢ 1 \in ℕ_{0}$
21	20	a1i	$⊢ (Rel F \land F \in V) \to 1 \in ℕ_{0}$
22		simpr	$⊢ (Rel F \land F \in V) \to F \in V$
23	13 19 21 22	fvmptd	$⊢ (Rel F \land F \in V) \to (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F)) (1) = F$
24	4 6 7 12 23	seqp1d	$⊢ (Rel F \land F \in V) \to seq 0 ((g \in V, j \in V ⟼ F \circ g), (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F))) (1) = ({I ↾}_{dom F}) (g \in V, j \in V ⟼ F \circ g) F$
25		eqidd	$⊢ F \in V \to (g \in V, j \in V ⟼ F \circ g) = (g \in V, j \in V ⟼ F \circ g)$
26		coeq2	$⊢ g = {I ↾}_{dom F} \to F \circ g = F \circ ({I ↾}_{dom F})$
27	26	ad2antrl	$⊢ (F \in V \land (g = {I ↾}_{dom F} \land j = F)) \to F \circ g = F \circ ({I ↾}_{dom F})$
28		dmexg	$⊢ F \in V \to dom F \in V$
29	28	resiexd	$⊢ F \in V \to {I ↾}_{dom F} \in V$
30		elex	$⊢ F \in V \to F \in V$
31		coexg	$⊢ (F \in V \land {I ↾}_{dom F} \in V) \to F \circ ({I ↾}_{dom F}) \in V$
32	29 31	mpdan	$⊢ F \in V \to F \circ ({I ↾}_{dom F}) \in V$
33	25 27 29 30 32	ovmpod	$⊢ F \in V \to ({I ↾}_{dom F}) (g \in V, j \in V ⟼ F \circ g) F = F \circ ({I ↾}_{dom F})$
34	33	adantl	$⊢ (Rel F \land F \in V) \to ({I ↾}_{dom F}) (g \in V, j \in V ⟼ F \circ g) F = F \circ ({I ↾}_{dom F})$
35		coires1	$⊢ F \circ ({I ↾}_{dom F}) = {F ↾}_{dom F}$
36		resdm	$⊢ Rel F \to {F ↾}_{dom F} = F$
37	36	adantr	$⊢ (Rel F \land F \in V) \to {F ↾}_{dom F} = F$
38	35 37	eqtrid	$⊢ (Rel F \land F \in V) \to F \circ ({I ↾}_{dom F}) = F$
39	34 38	eqtrd	$⊢ (Rel F \land F \in V) \to ({I ↾}_{dom F}) (g \in V, j \in V ⟼ F \circ g) F = F$
40	24 39	eqtrd	$⊢ (Rel F \land F \in V) \to seq 0 ((g \in V, j \in V ⟼ F \circ g), (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F))) (1) = F$
41	3 40	eqtrd	$⊢ (Rel F \land F \in V) \to IterComp (F) (1) = F$

Metamath Proof Explorer

Theorem itcoval1

Proof