This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ∃* 𝑓 𝑓 : 𝐴 ⟶ ∅