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	⊢ ∅ = ( 0g ‘ ∅ )

Proof

Step	Hyp	Ref	Expression
1		base0	⊢ ∅ = ( Base ‘ ∅ )
2		eqid	⊢ ( +g ‘ ∅ ) = ( +g ‘ ∅ )
3		eqid	⊢ ( 0g ‘ ∅ ) = ( 0g ‘ ∅ )
4	1 2 3	grpidval	⊢ ( 0g ‘ ∅ ) = ( ℩ 𝑒 ( 𝑒 ∈ ∅ ∧ ∀ 𝑥 ∈ ∅ ( ( 𝑒 ( +g ‘ ∅ ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ∅ ) 𝑒 ) = 𝑥 ) ) )
5		noel	⊢ ¬ 𝑒 ∈ ∅
6	5	intnanr	⊢ ¬ ( 𝑒 ∈ ∅ ∧ ∀ 𝑥 ∈ ∅ ( ( 𝑒 ( +g ‘ ∅ ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ∅ ) 𝑒 ) = 𝑥 ) )
7	6	nex	⊢ ¬ ∃ 𝑒 ( 𝑒 ∈ ∅ ∧ ∀ 𝑥 ∈ ∅ ( ( 𝑒 ( +g ‘ ∅ ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ∅ ) 𝑒 ) = 𝑥 ) )
8		euex	⊢ ( ∃! 𝑒 ( 𝑒 ∈ ∅ ∧ ∀ 𝑥 ∈ ∅ ( ( 𝑒 ( +g ‘ ∅ ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ∅ ) 𝑒 ) = 𝑥 ) ) → ∃ 𝑒 ( 𝑒 ∈ ∅ ∧ ∀ 𝑥 ∈ ∅ ( ( 𝑒 ( +g ‘ ∅ ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ∅ ) 𝑒 ) = 𝑥 ) ) )
9	7 8	mto	⊢ ¬ ∃! 𝑒 ( 𝑒 ∈ ∅ ∧ ∀ 𝑥 ∈ ∅ ( ( 𝑒 ( +g ‘ ∅ ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ∅ ) 𝑒 ) = 𝑥 ) )
10		iotanul	⊢ ( ¬ ∃! 𝑒 ( 𝑒 ∈ ∅ ∧ ∀ 𝑥 ∈ ∅ ( ( 𝑒 ( +g ‘ ∅ ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ∅ ) 𝑒 ) = 𝑥 ) ) → ( ℩ 𝑒 ( 𝑒 ∈ ∅ ∧ ∀ 𝑥 ∈ ∅ ( ( 𝑒 ( +g ‘ ∅ ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ∅ ) 𝑒 ) = 𝑥 ) ) ) = ∅ )
11	9 10	ax-mp	⊢ ( ℩ 𝑒 ( 𝑒 ∈ ∅ ∧ ∀ 𝑥 ∈ ∅ ( ( 𝑒 ( +g ‘ ∅ ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ∅ ) 𝑒 ) = 𝑥 ) ) ) = ∅
12	4 11	eqtr2i	⊢ ∅ = ( 0g ‘ ∅ )