Theorem naryfval

Description: The set of the n-ary (endo)functions on a class X . (Contributed by AV, 13-May-2024)

	Ref	Expression
Hypothesis	naryfval.i	$$⊢I=\left(0..^N\right)$$
Assertion	naryfval	Could not format assertion : No typesetting found for |- ( N e. NN0 -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		naryfval.i	$$⊢I=\left(0..^N\right)$$
2		simpr	$$⊢\left(n=N\wedge x=X\right)\to x=X$$
3		oveq2	$$⊢n=N\to \left(0..^n\right)=\left(0..^N\right)$$
4	3 1	eqtr4di	$$⊢n=N\to \left(0..^n\right)=I$$
5	4	adantr	$$⊢\left(n=N\wedge x=X\right)\to \left(0..^n\right)=I$$
6	2 5	oveq12d	$$⊢\left(n=N\wedge x=X\right)\to x^{\left(0..^n\right)}=X^I$$
7	2 6	oveq12d	$$⊢\left(n=N\wedge x=X\right)\to x^{\left(x^{\left(0..^n\right)}\right)}=X^{\left(X^I\right)}$$
8		df-naryf	Could not format -aryF = ( n e. NN0 , x e. _V |-> ( x ^m ( x ^m ( 0 ..^ n ) ) ) ) : No typesetting found for |- -aryF = ( n e. NN0 , x e. _V |-> ( x ^m ( x ^m ( 0 ..^ n ) ) ) ) with typecode |-
9		ovex	$$⊢X^{\left(X^I\right)}\in \mathrm{V}$$
10	7 8 9	ovmpoa	Could not format ( ( N e. NN0 /\ X e. _V ) -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) ) : No typesetting found for |- ( ( N e. NN0 /\ X e. _V ) -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) ) with typecode |-
11	10	ex	Could not format ( N e. NN0 -> ( X e. _V -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) ) ) : No typesetting found for |- ( N e. NN0 -> ( X e. _V -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) ) ) with typecode |-
12		simpr	$$⊢\left(N\in {\mathbb{N}}_0\wedge X\in \mathrm{V}\right)\to X\in \mathrm{V}$$
13		df-naryf	Could not format -aryF = ( x e. NN0 , n e. _V |-> ( n ^m ( n ^m ( 0 ..^ x ) ) ) ) : No typesetting found for |- -aryF = ( x e. NN0 , n e. _V |-> ( n ^m ( n ^m ( 0 ..^ x ) ) ) ) with typecode |-
14	13	mpondm0	Could not format ( -. ( N e. NN0 /\ X e. _V ) -> ( N -aryF X ) = (/) ) : No typesetting found for |- ( -. ( N e. NN0 /\ X e. _V ) -> ( N -aryF X ) = (/) ) with typecode |-
15	12 14	nsyl5	Could not format ( -. X e. _V -> ( N -aryF X ) = (/) ) : No typesetting found for |- ( -. X e. _V -> ( N -aryF X ) = (/) ) with typecode |-
16		simpl	$$⊢\left(X\in \mathrm{V}\wedge X^I\in \mathrm{V}\right)\to X\in \mathrm{V}$$
17		df-map	$$⊢{\uparrow }_{𝑚}=\left(x\in \mathrm{V},y\in \mathrm{V}⟼\left\{f|f:y⟶x\right\}\right)$$
18	17	mpondm0	$$⊢\neg \left(X\in \mathrm{V}\wedge X^I\in \mathrm{V}\right)\to X^{\left(X^I\right)}=\varnothing$$
19	16 18	nsyl5	$$⊢\neg X\in \mathrm{V}\to X^{\left(X^I\right)}=\varnothing$$
20	15 19	eqtr4d	Could not format ( -. X e. _V -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) ) : No typesetting found for |- ( -. X e. _V -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) ) with typecode |-
21	11 20	pm2.61d1	Could not format ( N e. NN0 -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) ) : No typesetting found for |- ( N e. NN0 -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) ) with typecode |-