Theorem smndex1gbas

Description: The constant functions ( GK ) are endofunctions on NN0 . (Contributed by AV, 12-Feb-2024) Avoid ax-rep and shorten proof. (Revised by GG, 2-Apr-2026)

	Ref	Expression
Hypotheses	smndex1ibas.m	⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
	smndex1ibas.n	⊢ 𝑁 ∈ ℕ
	smndex1ibas.i	⊢ 𝐼 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
	smndex1ibas.g	⊢ 𝐺 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) )
Assertion	smndex1gbas	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) ∈ ( Base ‘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		smndex1ibas.m	⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
2		smndex1ibas.n	⊢ 𝑁 ∈ ℕ
3		smndex1ibas.i	⊢ 𝐼 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
4		smndex1ibas.g	⊢ 𝐺 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) )
5		elfzonn0	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → 𝐾 ∈ ℕ0 )
6	5	adantr	⊢ ( ( 𝐾 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 ∈ ℕ0 ) → 𝐾 ∈ ℕ0 )
7	6	fmpttd	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) : ℕ0 ⟶ ℕ0 )
8		nn0ex	⊢ ℕ0 ∈ V
9	8 8	elmap	⊢ ( ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) ∈ ( ℕ0 ↑m ℕ0 ) ↔ ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) : ℕ0 ⟶ ℕ0 )
10	7 9	sylibr	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) ∈ ( ℕ0 ↑m ℕ0 ) )
11		id	⊢ ( 𝑛 = 𝐾 → 𝑛 = 𝐾 )
12	11	mpteq2dv	⊢ ( 𝑛 = 𝐾 → ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
13		fconstmpt	⊢ ( ℕ0 × { 𝐾 } ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 )
14		snex	⊢ { 𝐾 } ∈ V
15	8 14	xpex	⊢ ( ℕ0 × { 𝐾 } ) ∈ V
16	13 15	eqeltrri	⊢ ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) ∈ V
17	12 4 16	fvmpt	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
18		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
19	1 18	efmndbas	⊢ ( Base ‘ 𝑀 ) = ( ℕ0 ↑m ℕ0 )
20	19	a1i	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( Base ‘ 𝑀 ) = ( ℕ0 ↑m ℕ0 ) )
21	10 17 20	3eltr4d	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) ∈ ( Base ‘ 𝑀 ) )