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	⊢ ( 𝑋 ∈ 𝑉 → ( 𝐹 ∈ ( 0 -aryF 𝑋 ) ↔ ∃ 𝑥 ∈ 𝑋 𝐹 = { ⟨ ∅ , 𝑥 ⟩ } ) )

Proof

Step	Hyp	Ref	Expression
1		0nn0	⊢ 0 ∈ ℕ0
2		fzo0	⊢ ( 0 ..^ 0 ) = ∅
3	2	eqcomi	⊢ ∅ = ( 0 ..^ 0 )
4	3	naryfvalel	⊢ ( ( 0 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 ∈ ( 0 -aryF 𝑋 ) ↔ 𝐹 : ( 𝑋 ↑m ∅ ) ⟶ 𝑋 ) )
5	1 4	mpan	⊢ ( 𝑋 ∈ 𝑉 → ( 𝐹 ∈ ( 0 -aryF 𝑋 ) ↔ 𝐹 : ( 𝑋 ↑m ∅ ) ⟶ 𝑋 ) )
6		mapdm0	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ↑m ∅ ) = { ∅ } )
7	6	feq2d	⊢ ( 𝑋 ∈ 𝑉 → ( 𝐹 : ( 𝑋 ↑m ∅ ) ⟶ 𝑋 ↔ 𝐹 : { ∅ } ⟶ 𝑋 ) )
8		0ex	⊢ ∅ ∈ V
9	8	fsn2	⊢ ( 𝐹 : { ∅ } ⟶ 𝑋 ↔ ( ( 𝐹 ‘ ∅ ) ∈ 𝑋 ∧ 𝐹 = { ⟨ ∅ , ( 𝐹 ‘ ∅ ) ⟩ } ) )
10		opeq2	⊢ ( 𝑥 = ( 𝐹 ‘ ∅ ) → ⟨ ∅ , 𝑥 ⟩ = ⟨ ∅ , ( 𝐹 ‘ ∅ ) ⟩ )
11	10	sneqd	⊢ ( 𝑥 = ( 𝐹 ‘ ∅ ) → { ⟨ ∅ , 𝑥 ⟩ } = { ⟨ ∅ , ( 𝐹 ‘ ∅ ) ⟩ } )
12	11	rspceeqv	⊢ ( ( ( 𝐹 ‘ ∅ ) ∈ 𝑋 ∧ 𝐹 = { ⟨ ∅ , ( 𝐹 ‘ ∅ ) ⟩ } ) → ∃ 𝑥 ∈ 𝑋 𝐹 = { ⟨ ∅ , 𝑥 ⟩ } )
13	9 12	sylbi	⊢ ( 𝐹 : { ∅ } ⟶ 𝑋 → ∃ 𝑥 ∈ 𝑋 𝐹 = { ⟨ ∅ , 𝑥 ⟩ } )
14	8	a1i	⊢ ( 𝑥 ∈ 𝑋 → ∅ ∈ V )
15		id	⊢ ( 𝑥 ∈ 𝑋 → 𝑥 ∈ 𝑋 )
16	14 15	fsnd	⊢ ( 𝑥 ∈ 𝑋 → { ⟨ ∅ , 𝑥 ⟩ } : { ∅ } ⟶ 𝑋 )
17		feq1	⊢ ( 𝐹 = { ⟨ ∅ , 𝑥 ⟩ } → ( 𝐹 : { ∅ } ⟶ 𝑋 ↔ { ⟨ ∅ , 𝑥 ⟩ } : { ∅ } ⟶ 𝑋 ) )
18	16 17	syl5ibrcom	⊢ ( 𝑥 ∈ 𝑋 → ( 𝐹 = { ⟨ ∅ , 𝑥 ⟩ } → 𝐹 : { ∅ } ⟶ 𝑋 ) )
19	18	rexlimiv	⊢ ( ∃ 𝑥 ∈ 𝑋 𝐹 = { ⟨ ∅ , 𝑥 ⟩ } → 𝐹 : { ∅ } ⟶ 𝑋 )
20	13 19	impbii	⊢ ( 𝐹 : { ∅ } ⟶ 𝑋 ↔ ∃ 𝑥 ∈ 𝑋 𝐹 = { ⟨ ∅ , 𝑥 ⟩ } )
21	20	a1i	⊢ ( 𝑋 ∈ 𝑉 → ( 𝐹 : { ∅ } ⟶ 𝑋 ↔ ∃ 𝑥 ∈ 𝑋 𝐹 = { ⟨ ∅ , 𝑥 ⟩ } ) )
22	5 7 21	3bitrd	⊢ ( 𝑋 ∈ 𝑉 → ( 𝐹 ∈ ( 0 -aryF 𝑋 ) ↔ ∃ 𝑥 ∈ 𝑋 𝐹 = { ⟨ ∅ , 𝑥 ⟩ } ) )