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 ⊢ F ∈ 0 -aryF X → ∃ x ∈ X F ⁡ ∅ = x

Proof

Step Hyp Ref Expression
1 eqid ⊢ 0 ..^ 0 = 0 ..^ 0
2 1 naryrcl ⊢ F ∈ 0 -aryF X → 0 ∈ ℕ 0 ∧ X ∈ V
3 0aryfvalel ⊢ X ∈ V → F ∈ 0 -aryF X ↔ ∃ x ∈ X F = ∅ x
4 0ex ⊢ ∅ ∈ V
5 fvsng ⊢ ∅ ∈ V ∧ x ∈ X → ∅ x ⁡ ∅ = x
6 4 5 mpan ⊢ x ∈ X → ∅ x ⁡ ∅ = x
7 fveq1 ⊢ F = ∅ x → F ⁡ ∅ = ∅ x ⁡ ∅
8 7 eqeq1d ⊢ F = ∅ x → F ⁡ ∅ = x ↔ ∅ x ⁡ ∅ = x
9 6 8 syl5ibrcom ⊢ x ∈ X → F = ∅ x → F ⁡ ∅ = x
10 9 reximia ⊢ ∃ x ∈ X F = ∅ x → ∃ x ∈ X F ⁡ ∅ = x
11 3 10 biimtrdi ⊢ X ∈ V → F ∈ 0 -aryF X → ∃ x ∈ X F ⁡ ∅ = x
12 11 adantl ⊢ 0 ∈ ℕ 0 ∧ X ∈ V → F ∈ 0 -aryF X → ∃ x ∈ X F ⁡ ∅ = x
13 2 12 mpcom ⊢ F ∈ 0 -aryF X → ∃ x ∈ X F ⁡ ∅ = x