Theorem mof0

Description: There is at most one function into the empty set. (Contributed by Zhi Wang, 19-Sep-2024)

	Ref	Expression
Assertion	mof0	⊢ ∃* 𝑓 𝑓 : 𝐴 ⟶ ∅

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2		eqeq2	⊢ ( 𝑔 = ∅ → ( 𝑓 = 𝑔 ↔ 𝑓 = ∅ ) )
3	2	imbi2d	⊢ ( 𝑔 = ∅ → ( ( 𝑓 : 𝐴 ⟶ ∅ → 𝑓 = 𝑔 ) ↔ ( 𝑓 : 𝐴 ⟶ ∅ → 𝑓 = ∅ ) ) )
4	3	albidv	⊢ ( 𝑔 = ∅ → ( ∀ 𝑓 ( 𝑓 : 𝐴 ⟶ ∅ → 𝑓 = 𝑔 ) ↔ ∀ 𝑓 ( 𝑓 : 𝐴 ⟶ ∅ → 𝑓 = ∅ ) ) )
5	1 4	spcev	⊢ ( ∀ 𝑓 ( 𝑓 : 𝐴 ⟶ ∅ → 𝑓 = ∅ ) → ∃ 𝑔 ∀ 𝑓 ( 𝑓 : 𝐴 ⟶ ∅ → 𝑓 = 𝑔 ) )
6		f00	⊢ ( 𝑓 : 𝐴 ⟶ ∅ ↔ ( 𝑓 = ∅ ∧ 𝐴 = ∅ ) )
7	6	simplbi	⊢ ( 𝑓 : 𝐴 ⟶ ∅ → 𝑓 = ∅ )
8	5 7	mpg	⊢ ∃ 𝑔 ∀ 𝑓 ( 𝑓 : 𝐴 ⟶ ∅ → 𝑓 = 𝑔 )
9		df-mo	⊢ ( ∃* 𝑓 𝑓 : 𝐴 ⟶ ∅ ↔ ∃ 𝑔 ∀ 𝑓 ( 𝑓 : 𝐴 ⟶ ∅ → 𝑓 = 𝑔 ) )
10	8 9	mpbir	⊢ ∃* 𝑓 𝑓 : 𝐴 ⟶ ∅