Theorem 0aryfvalelfv

Description: The value of a nullary (endo)function on a set X . (Contributed by AV, 19-May-2024)

	Ref	Expression
Assertion	0aryfvalelfv	⊢ ( 𝐹 ∈ ( 0 -aryF 𝑋 ) → ∃ 𝑥 ∈ 𝑋 ( 𝐹 ‘ ∅ ) = 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 0 ..^ 0 ) = ( 0 ..^ 0 )
2	1	naryrcl	⊢ ( 𝐹 ∈ ( 0 -aryF 𝑋 ) → ( 0 ∈ ℕ0 ∧ 𝑋 ∈ V ) )
3		0aryfvalel	⊢ ( 𝑋 ∈ V → ( 𝐹 ∈ ( 0 -aryF 𝑋 ) ↔ ∃ 𝑥 ∈ 𝑋 𝐹 = { ⟨ ∅ , 𝑥 ⟩ } ) )
4		0ex	⊢ ∅ ∈ V
5		fvsng	⊢ ( ( ∅ ∈ V ∧ 𝑥 ∈ 𝑋 ) → ( { ⟨ ∅ , 𝑥 ⟩ } ‘ ∅ ) = 𝑥 )
6	4 5	mpan	⊢ ( 𝑥 ∈ 𝑋 → ( { ⟨ ∅ , 𝑥 ⟩ } ‘ ∅ ) = 𝑥 )
7		fveq1	⊢ ( 𝐹 = { ⟨ ∅ , 𝑥 ⟩ } → ( 𝐹 ‘ ∅ ) = ( { ⟨ ∅ , 𝑥 ⟩ } ‘ ∅ ) )
8	7	eqeq1d	⊢ ( 𝐹 = { ⟨ ∅ , 𝑥 ⟩ } → ( ( 𝐹 ‘ ∅ ) = 𝑥 ↔ ( { ⟨ ∅ , 𝑥 ⟩ } ‘ ∅ ) = 𝑥 ) )
9	6 8	syl5ibrcom	⊢ ( 𝑥 ∈ 𝑋 → ( 𝐹 = { ⟨ ∅ , 𝑥 ⟩ } → ( 𝐹 ‘ ∅ ) = 𝑥 ) )
10	9	reximia	⊢ ( ∃ 𝑥 ∈ 𝑋 𝐹 = { ⟨ ∅ , 𝑥 ⟩ } → ∃ 𝑥 ∈ 𝑋 ( 𝐹 ‘ ∅ ) = 𝑥 )
11	3 10	biimtrdi	⊢ ( 𝑋 ∈ V → ( 𝐹 ∈ ( 0 -aryF 𝑋 ) → ∃ 𝑥 ∈ 𝑋 ( 𝐹 ‘ ∅ ) = 𝑥 ) )
12	11	adantl	⊢ ( ( 0 ∈ ℕ0 ∧ 𝑋 ∈ V ) → ( 𝐹 ∈ ( 0 -aryF 𝑋 ) → ∃ 𝑥 ∈ 𝑋 ( 𝐹 ‘ ∅ ) = 𝑥 ) )
13	2 12	mpcom	⊢ ( 𝐹 ∈ ( 0 -aryF 𝑋 ) → ∃ 𝑥 ∈ 𝑋 ( 𝐹 ‘ ∅ ) = 𝑥 )