Theorem 0aryfvalelfv

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

	Ref	Expression
Assertion	0aryfvalelfv	Could not format assertion : No typesetting found for |- ( F e. ( 0 -aryF X ) -> E. x e. X ( F ` (/) ) = x ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left(0..^0\right)=\left(0..^0\right)$$
2	1	naryrcl	Could not format ( F e. ( 0 -aryF X ) -> ( 0 e. NN0 /\ X e. _V ) ) : No typesetting found for |- ( F e. ( 0 -aryF X ) -> ( 0 e. NN0 /\ X e. _V ) ) with typecode |-
3		0aryfvalel	Could not format ( X e. _V -> ( F e. ( 0 -aryF X ) <-> E. x e. X F = { <. (/) , x >. } ) ) : No typesetting found for |- ( X e. _V -> ( F e. ( 0 -aryF X ) <-> E. x e. X F = { <. (/) , x >. } ) ) with typecode |-
4		0ex	$$⊢\varnothing \in \mathrm{V}$$
5		fvsng	$$⊢\left(\varnothing \in \mathrm{V}\wedge x\in X\right)\to \left\{⟨\varnothing ,x⟩\right\}\left(\varnothing \right)=x$$
6	4 5	mpan	$$⊢x\in X\to \left\{⟨\varnothing ,x⟩\right\}\left(\varnothing \right)=x$$
7		fveq1	$$⊢F=\left\{⟨\varnothing ,x⟩\right\}\to F\left(\varnothing \right)=\left\{⟨\varnothing ,x⟩\right\}\left(\varnothing \right)$$
8	7	eqeq1d	$$⊢F=\left\{⟨\varnothing ,x⟩\right\}\to \left(F\left(\varnothing \right)=x\leftrightarrow \left\{⟨\varnothing ,x⟩\right\}\left(\varnothing \right)=x\right)$$
9	6 8	syl5ibrcom	$$⊢x\in X\to \left(F=\left\{⟨\varnothing ,x⟩\right\}\to F\left(\varnothing \right)=x\right)$$
10	9	reximia	$$⊢\exists x\in XF=\left\{⟨\varnothing ,x⟩\right\}\to \exists x\in XF\left(\varnothing \right)=x$$
11	3 10	syl6bi	Could not format ( X e. _V -> ( F e. ( 0 -aryF X ) -> E. x e. X ( F ` (/) ) = x ) ) : No typesetting found for |- ( X e. _V -> ( F e. ( 0 -aryF X ) -> E. x e. X ( F ` (/) ) = x ) ) with typecode |-
12	11	adantl	Could not format ( ( 0 e. NN0 /\ X e. _V ) -> ( F e. ( 0 -aryF X ) -> E. x e. X ( F ` (/) ) = x ) ) : No typesetting found for |- ( ( 0 e. NN0 /\ X e. _V ) -> ( F e. ( 0 -aryF X ) -> E. x e. X ( F ` (/) ) = x ) ) with typecode |-
13	2 12	mpcom	Could not format ( F e. ( 0 -aryF X ) -> E. x e. X ( F ` (/) ) = x ) : No typesetting found for |- ( F e. ( 0 -aryF X ) -> E. x e. X ( F ` (/) ) = x ) with typecode |-