Metamath Proof Explorer


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 syl6bi ( 𝑋 ∈ V → ( 𝐹 ∈ ( 0 -aryF 𝑋 ) → ∃ 𝑥𝑋 ( 𝐹 ‘ ∅ ) = 𝑥 ) )
12 11 adantl ( ( 0 ∈ ℕ0𝑋 ∈ V ) → ( 𝐹 ∈ ( 0 -aryF 𝑋 ) → ∃ 𝑥𝑋 ( 𝐹 ‘ ∅ ) = 𝑥 ) )
13 2 12 mpcom ( 𝐹 ∈ ( 0 -aryF 𝑋 ) → ∃ 𝑥𝑋 ( 𝐹 ‘ ∅ ) = 𝑥 )