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	⊢ 𝐼 = ( 0 ..^ 𝑁 )
Assertion	naryfvalixp	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 -aryF 𝑋 ) = ( 𝑋 ↑m X 𝑥 ∈ 𝐼 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		naryfval.i	⊢ 𝐼 = ( 0 ..^ 𝑁 )
2	1	naryfval	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 -aryF 𝑋 ) = ( 𝑋 ↑m ( 𝑋 ↑m 𝐼 ) ) )
3	2	adantr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ V ) → ( 𝑁 -aryF 𝑋 ) = ( 𝑋 ↑m ( 𝑋 ↑m 𝐼 ) ) )
4	1	ovexi	⊢ 𝐼 ∈ V
5	4	a1i	⊢ ( 𝑁 ∈ ℕ0 → 𝐼 ∈ V )
6		ixpconstg	⊢ ( ( 𝐼 ∈ V ∧ 𝑋 ∈ V ) → X 𝑥 ∈ 𝐼 𝑋 = ( 𝑋 ↑m 𝐼 ) )
7	5 6	sylan	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ V ) → X 𝑥 ∈ 𝐼 𝑋 = ( 𝑋 ↑m 𝐼 ) )
8	7	oveq2d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ V ) → ( 𝑋 ↑m X 𝑥 ∈ 𝐼 𝑋 ) = ( 𝑋 ↑m ( 𝑋 ↑m 𝐼 ) ) )
9	3 8	eqtr4d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ V ) → ( 𝑁 -aryF 𝑋 ) = ( 𝑋 ↑m X 𝑥 ∈ 𝐼 𝑋 ) )
10	9	ex	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑋 ∈ V → ( 𝑁 -aryF 𝑋 ) = ( 𝑋 ↑m X 𝑥 ∈ 𝐼 𝑋 ) ) )
11		simpr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ V ) → 𝑋 ∈ V )
12		df-naryf	⊢ -aryF = ( 𝑥 ∈ ℕ0 , 𝑛 ∈ V ↦ ( 𝑛 ↑m ( 𝑛 ↑m ( 0 ..^ 𝑥 ) ) ) )
13	12	mpondm0	⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ V ) → ( 𝑁 -aryF 𝑋 ) = ∅ )
14	11 13	nsyl5	⊢ ( ¬ 𝑋 ∈ V → ( 𝑁 -aryF 𝑋 ) = ∅ )
15		reldmmap	⊢ Rel dom ↑m
16	15	ovprc1	⊢ ( ¬ 𝑋 ∈ V → ( 𝑋 ↑m X 𝑥 ∈ 𝐼 𝑋 ) = ∅ )
17	14 16	eqtr4d	⊢ ( ¬ 𝑋 ∈ V → ( 𝑁 -aryF 𝑋 ) = ( 𝑋 ↑m X 𝑥 ∈ 𝐼 𝑋 ) )
18	10 17	pm2.61d1	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 -aryF 𝑋 ) = ( 𝑋 ↑m X 𝑥 ∈ 𝐼 𝑋 ) )