Theorem 0aryfvalel

Description: A nullary (endo)function on a set X is a singleton of an ordered pair with the empty set as first component. A nullary function represents a constant: ( F(/) ) = C with C e. X , see also 0aryfvalelfv . Instead of ( F(/) ) , nullary functions are usually written as F ( ) in literature. (Contributed by AV, 15-May-2024)

	Ref	Expression
Assertion	0aryfvalel	$$⊢X\in V\to \left(F\in \left(0\mathrm{-aryF}X\right)\leftrightarrow \exists x\in XF=\left\{⟨\varnothing ,x⟩\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		0nn0	$$⊢0\in {\mathbb{N}}_0$$
2		fzo0	$$⊢\left(0..^0\right)=\varnothing$$
3	2	eqcomi	$$⊢\varnothing =\left(0..^0\right)$$
4	3	naryfvalel	$$⊢\left(0\in {\mathbb{N}}_0\wedge X\in V\right)\to \left(F\in \left(0\mathrm{-aryF}X\right)\leftrightarrow F:X^{\varnothing }⟶X\right)$$
5	1 4	mpan	$$⊢X\in V\to \left(F\in \left(0\mathrm{-aryF}X\right)\leftrightarrow F:X^{\varnothing }⟶X\right)$$
6		mapdm0	$$⊢X\in V\to X^{\varnothing }=\left\{\varnothing \right\}$$
7	6	feq2d	$$⊢X\in V\to \left(F:X^{\varnothing }⟶X\leftrightarrow F:\left\{\varnothing \right\}⟶X\right)$$
8		0ex	$$⊢\varnothing \in \mathrm{V}$$
9	8	fsn2	$$⊢F:\left\{\varnothing \right\}⟶X\leftrightarrow \left(F\left(\varnothing \right)\in X\wedge F=\left\{⟨\varnothing ,F\left(\varnothing \right)⟩\right\}\right)$$
10		opeq2	$$⊢x=F\left(\varnothing \right)\to ⟨\varnothing ,x⟩=⟨\varnothing ,F\left(\varnothing \right)⟩$$
11	10	sneqd	$$⊢x=F\left(\varnothing \right)\to \left\{⟨\varnothing ,x⟩\right\}=\left\{⟨\varnothing ,F\left(\varnothing \right)⟩\right\}$$
12	11	rspceeqv	$$⊢\left(F\left(\varnothing \right)\in X\wedge F=\left\{⟨\varnothing ,F\left(\varnothing \right)⟩\right\}\right)\to \exists x\in XF=\left\{⟨\varnothing ,x⟩\right\}$$
13	9 12	sylbi	$$⊢F:\left\{\varnothing \right\}⟶X\to \exists x\in XF=\left\{⟨\varnothing ,x⟩\right\}$$
14	8	a1i	$$⊢x\in X\to \varnothing \in \mathrm{V}$$
15		id	$$⊢x\in X\to x\in X$$
16	14 15	fsnd	$$⊢x\in X\to \left\{⟨\varnothing ,x⟩\right\}:\left\{\varnothing \right\}⟶X$$
17		feq1	$$⊢F=\left\{⟨\varnothing ,x⟩\right\}\to \left(F:\left\{\varnothing \right\}⟶X\leftrightarrow \left\{⟨\varnothing ,x⟩\right\}:\left\{\varnothing \right\}⟶X\right)$$
18	16 17	syl5ibrcom	$$⊢x\in X\to \left(F=\left\{⟨\varnothing ,x⟩\right\}\to F:\left\{\varnothing \right\}⟶X\right)$$
19	18	rexlimiv	$$⊢\exists x\in XF=\left\{⟨\varnothing ,x⟩\right\}\to F:\left\{\varnothing \right\}⟶X$$
20	13 19	impbii	$$⊢F:\left\{\varnothing \right\}⟶X\leftrightarrow \exists x\in XF=\left\{⟨\varnothing ,x⟩\right\}$$
21	20	a1i	$$⊢X\in V\to \left(F:\left\{\varnothing \right\}⟶X\leftrightarrow \exists x\in XF=\left\{⟨\varnothing ,x⟩\right\}\right)$$
22	5 7 21	3bitrd	$$⊢X\in V\to \left(F\in \left(0\mathrm{-aryF}X\right)\leftrightarrow \exists x\in XF=\left\{⟨\varnothing ,x⟩\right\}\right)$$