Theorem itcoval0mpt

Description: A mapping iterated zero times (defined as identity function). (Contributed by AV, 4-May-2024)

	Ref	Expression
Hypothesis	itcoval0mpt.f	$$⊢F=\left(n\in A⟼B\right)$$
Assertion	itcoval0mpt	Could not format assertion : No typesetting found for |- ( ( A e. V /\ A. n e. A B e. W ) -> ( ( IterComp ` F ) ` 0 ) = ( n e. A |-> n ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		itcoval0mpt.f	$$⊢F=\left(n\in A⟼B\right)$$
2	1	fveq2i	Could not format ( IterComp ` F ) = ( IterComp ` ( n e. A |-> B ) ) : No typesetting found for |- ( IterComp ` F ) = ( IterComp ` ( n e. A |-> B ) ) with typecode |-
3	2	fveq1i	Could not format ( ( IterComp ` F ) ` 0 ) = ( ( IterComp ` ( n e. A |-> B ) ) ` 0 ) : No typesetting found for |- ( ( IterComp ` F ) ` 0 ) = ( ( IterComp ` ( n e. A |-> B ) ) ` 0 ) with typecode |-
4		mptexg	$$⊢A\in V\to \left(n\in A⟼B\right)\in \mathrm{V}$$
5		itcoval0	Could not format ( ( n e. A |-> B ) e. _V -> ( ( IterComp ` ( n e. A |-> B ) ) ` 0 ) = ( _I |` dom ( n e. A |-> B ) ) ) : No typesetting found for |- ( ( n e. A |-> B ) e. _V -> ( ( IterComp ` ( n e. A |-> B ) ) ` 0 ) = ( _I |` dom ( n e. A |-> B ) ) ) with typecode |-
6	4 5	syl	Could not format ( A e. V -> ( ( IterComp ` ( n e. A |-> B ) ) ` 0 ) = ( _I |` dom ( n e. A |-> B ) ) ) : No typesetting found for |- ( A e. V -> ( ( IterComp ` ( n e. A |-> B ) ) ` 0 ) = ( _I |` dom ( n e. A |-> B ) ) ) with typecode |-
7	3 6	syl5eq	Could not format ( A e. V -> ( ( IterComp ` F ) ` 0 ) = ( _I |` dom ( n e. A |-> B ) ) ) : No typesetting found for |- ( A e. V -> ( ( IterComp ` F ) ` 0 ) = ( _I |` dom ( n e. A |-> B ) ) ) with typecode |-
8		dmmptg	$$⊢\forall n\in AB\in W\to \mathrm{dom}\left(n\in A⟼B\right)=A$$
9	8	reseq2d	$$⊢\forall n\in AB\in W\to {\mathrm{I}\upharpoonright }_{\mathrm{dom}\left(n\in A⟼B\right)}={\mathrm{I}\upharpoonright }_A$$
10		mptresid	$$⊢{\mathrm{I}\upharpoonright }_A=\left(n\in A⟼n\right)$$
11	9 10	eqtrdi	$$⊢\forall n\in AB\in W\to {\mathrm{I}\upharpoonright }_{\mathrm{dom}\left(n\in A⟼B\right)}=\left(n\in A⟼n\right)$$
12	7 11	sylan9eq	Could not format ( ( A e. V /\ A. n e. A B e. W ) -> ( ( IterComp ` F ) ` 0 ) = ( n e. A |-> n ) ) : No typesetting found for |- ( ( A e. V /\ A. n e. A B e. W ) -> ( ( IterComp ` F ) ` 0 ) = ( n e. A |-> n ) ) with typecode |-