Theorem fv1arycl

Description: Closure of a unary (endo)function. (Contributed by AV, 18-May-2024)

	Ref	Expression
Assertion	fv1arycl	⊢ ( ( 𝐺 ∈ ( 1 -aryF 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐺 ‘ { ⟨ 0 , 𝐴 ⟩ } ) ∈ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 0 ..^ 1 ) = ( 0 ..^ 1 )
2	1	naryrcl	⊢ ( 𝐺 ∈ ( 1 -aryF 𝑋 ) → ( 1 ∈ ℕ0 ∧ 𝑋 ∈ V ) )
3		1aryfvalel	⊢ ( 𝑋 ∈ V → ( 𝐺 ∈ ( 1 -aryF 𝑋 ) ↔ 𝐺 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ) )
4		simp2	⊢ ( ( 𝑋 ∈ V ∧ 𝐺 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → 𝐺 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 )
5		c0ex	⊢ 0 ∈ V
6	5	a1i	⊢ ( ( 𝑋 ∈ V ∧ 𝐺 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → 0 ∈ V )
7		simp3	⊢ ( ( 𝑋 ∈ V ∧ 𝐺 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
8	6 7	fsnd	⊢ ( ( 𝑋 ∈ V ∧ 𝐺 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → { ⟨ 0 , 𝐴 ⟩ } : { 0 } ⟶ 𝑋 )
9		simp1	⊢ ( ( 𝑋 ∈ V ∧ 𝐺 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → 𝑋 ∈ V )
10		snex	⊢ { 0 } ∈ V
11	10	a1i	⊢ ( ( 𝑋 ∈ V ∧ 𝐺 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → { 0 } ∈ V )
12	9 11	elmapd	⊢ ( ( 𝑋 ∈ V ∧ 𝐺 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( { ⟨ 0 , 𝐴 ⟩ } ∈ ( 𝑋 ↑m { 0 } ) ↔ { ⟨ 0 , 𝐴 ⟩ } : { 0 } ⟶ 𝑋 ) )
13	8 12	mpbird	⊢ ( ( 𝑋 ∈ V ∧ 𝐺 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → { ⟨ 0 , 𝐴 ⟩ } ∈ ( 𝑋 ↑m { 0 } ) )
14	4 13	ffvelrnd	⊢ ( ( 𝑋 ∈ V ∧ 𝐺 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐺 ‘ { ⟨ 0 , 𝐴 ⟩ } ) ∈ 𝑋 )
15	14	3exp	⊢ ( 𝑋 ∈ V → ( 𝐺 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 → ( 𝐴 ∈ 𝑋 → ( 𝐺 ‘ { ⟨ 0 , 𝐴 ⟩ } ) ∈ 𝑋 ) ) )
16	3 15	sylbid	⊢ ( 𝑋 ∈ V → ( 𝐺 ∈ ( 1 -aryF 𝑋 ) → ( 𝐴 ∈ 𝑋 → ( 𝐺 ‘ { ⟨ 0 , 𝐴 ⟩ } ) ∈ 𝑋 ) ) )
17	16	adantl	⊢ ( ( 1 ∈ ℕ0 ∧ 𝑋 ∈ V ) → ( 𝐺 ∈ ( 1 -aryF 𝑋 ) → ( 𝐴 ∈ 𝑋 → ( 𝐺 ‘ { ⟨ 0 , 𝐴 ⟩ } ) ∈ 𝑋 ) ) )
18	2 17	mpcom	⊢ ( 𝐺 ∈ ( 1 -aryF 𝑋 ) → ( 𝐴 ∈ 𝑋 → ( 𝐺 ‘ { ⟨ 0 , 𝐴 ⟩ } ) ∈ 𝑋 ) )
19	18	imp	⊢ ( ( 𝐺 ∈ ( 1 -aryF 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐺 ‘ { ⟨ 0 , 𝐴 ⟩ } ) ∈ 𝑋 )