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

Metamath Proof Explorer

Theorem 0map0sn0

Description: The set of mappings of the empty set to the empty set is the singleton containing the empty set. (Contributed by AV, 31-Mar-2024)

Ref Expression
Assertion 0map0sn0 ( ∅ ↑m ∅ ) = { ∅ }

Proof

Step Hyp Ref Expression
1 f0bi ⊢ ( 𝑓 : ∅ ⟶ ∅ ↔ 𝑓 = ∅ )
2 1 abbii ⊢ { 𝑓 ∣ 𝑓 : ∅ ⟶ ∅ } = { 𝑓 ∣ 𝑓 = ∅ }
3 0ex ⊢ ∅ ∈ V
4 3 3 mapval ⊢ ( ∅ ↑m ∅ ) = { 𝑓 ∣ 𝑓 : ∅ ⟶ ∅ }
5 df-sn ⊢ { ∅ } = { 𝑓 ∣ 𝑓 = ∅ }
6 2 4 5 3eqtr4i ⊢ ( ∅ ↑m ∅ ) = { ∅ }