Metamath Proof Explorer

Theorem 0g0

Description: The identity element function evaluates to the empty set on an empty structure. (Contributed by Stefan O'Rear, 2-Oct-2015)

Ref Expression
Assertion 0g0 ⊢ ∅ = 0 ∅

Proof

Step Hyp Ref Expression
1 base0 ⊢ ∅ = Base ∅
2 eqid ⊢ + ∅ = + ∅
3 eqid ⊢ 0 ∅ = 0 ∅
4 1 2 3 grpidval ⊢ 0 ∅ = ι e | e ∈ ∅ ∧ ∀ x ∈ ∅ e + ∅ x = x ∧ x + ∅ e = x
5 noel ⊢ ¬ e ∈ ∅
6 5 intnanr ⊢ ¬ e ∈ ∅ ∧ ∀ x ∈ ∅ e + ∅ x = x ∧ x + ∅ e = x
7 6 nex ⊢ ¬ ∃ e e ∈ ∅ ∧ ∀ x ∈ ∅ e + ∅ x = x ∧ x + ∅ e = x
8 euex ⊢ ∃! e e ∈ ∅ ∧ ∀ x ∈ ∅ e + ∅ x = x ∧ x + ∅ e = x → ∃ e e ∈ ∅ ∧ ∀ x ∈ ∅ e + ∅ x = x ∧ x + ∅ e = x
9 7 8 mto ⊢ ¬ ∃! e e ∈ ∅ ∧ ∀ x ∈ ∅ e + ∅ x = x ∧ x + ∅ e = x
10 iotanul ⊢ ¬ ∃! e e ∈ ∅ ∧ ∀ x ∈ ∅ e + ∅ x = x ∧ x + ∅ e = x → ι e | e ∈ ∅ ∧ ∀ x ∈ ∅ e + ∅ x = x ∧ x + ∅ e = x = ∅
11 9 10 ax-mp ⊢ ι e | e ∈ ∅ ∧ ∀ x ∈ ∅ e + ∅ x = x ∧ x + ∅ e = x = ∅
12 4 11 eqtr2i ⊢ ∅ = 0 ∅