Theorem naryfvalixp

Description: The set of the n-ary (endo)functions on a class X expressed with the notation of infinite Cartesian products. (Contributed by AV, 19-May-2024)

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

Proof

Step	Hyp	Ref	Expression
1		naryfval.i	$$⊢I=\left(0..^N\right)$$
2	1	naryfval	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 |-
3	2	adantr	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 |-
4	1	ovexi	$$⊢I\in \mathrm{V}$$
5	4	a1i	$$⊢N\in {\mathbb{N}}_0\to I\in \mathrm{V}$$
6		ixpconstg	$$⊢\left(I\in \mathrm{V}\wedge X\in \mathrm{V}\right)\to \underset{x\in I}{⨉}X=X^I$$
7	5 6	sylan	$$⊢\left(N\in {\mathbb{N}}_0\wedge X\in \mathrm{V}\right)\to \underset{x\in I}{⨉}X=X^I$$
8	7	oveq2d	$$⊢\left(N\in {\mathbb{N}}_0\wedge X\in \mathrm{V}\right)\to X^{\underset{x\in I}{⨉}X}=X^{\left(X^I\right)}$$
9	3 8	eqtr4d	Could not format ( ( N e. NN0 /\ X e. _V ) -> ( N -aryF X ) = ( X ^m X_ x e. I X ) ) : No typesetting found for |- ( ( N e. NN0 /\ X e. _V ) -> ( N -aryF X ) = ( X ^m X_ x e. I X ) ) with typecode |-
10	9	ex	Could not format ( N e. NN0 -> ( X e. _V -> ( N -aryF X ) = ( X ^m X_ x e. I X ) ) ) : No typesetting found for |- ( N e. NN0 -> ( X e. _V -> ( N -aryF X ) = ( X ^m X_ x e. I X ) ) ) with typecode |-
11		simpr	$$⊢\left(N\in {\mathbb{N}}_0\wedge X\in \mathrm{V}\right)\to X\in \mathrm{V}$$
12		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 |-
13	12	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 |-
14	11 13	nsyl5	Could not format ( -. X e. _V -> ( N -aryF X ) = (/) ) : No typesetting found for |- ( -. X e. _V -> ( N -aryF X ) = (/) ) with typecode |-
15		reldmmap	$$⊢\mathrm{Rel}\mathrm{dom}{\uparrow }_{𝑚}$$
16	15	ovprc1	$$⊢\neg X\in \mathrm{V}\to X^{\underset{x\in I}{⨉}X}=\varnothing$$
17	14 16	eqtr4d	Could not format ( -. X e. _V -> ( N -aryF X ) = ( X ^m X_ x e. I X ) ) : No typesetting found for |- ( -. X e. _V -> ( N -aryF X ) = ( X ^m X_ x e. I X ) ) with typecode |-
18	10 17	pm2.61d1	Could not format ( N e. NN0 -> ( N -aryF X ) = ( X ^m X_ x e. I X ) ) : No typesetting found for |- ( N e. NN0 -> ( N -aryF X ) = ( X ^m X_ x e. I X ) ) with typecode |-