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 
|- (/) = ( 0g ` (/) )

Proof

Step Hyp Ref Expression
1 base0 
 |-  (/) = ( Base ` (/) )
2 eqid 
 |-  ( +g ` (/) ) = ( +g ` (/) )
3 eqid 
 |-  ( 0g ` (/) ) = ( 0g ` (/) )
4 1 2 3 grpidval 
 |-  ( 0g ` (/) ) = ( iota e ( e e. (/) /\ A. x e. (/) ( ( e ( +g ` (/) ) x ) = x /\ ( x ( +g ` (/) ) e ) = x ) ) )
5 noel 
 |-  -. e e. (/)
6 5 intnanr 
 |-  -. ( e e. (/) /\ A. x e. (/) ( ( e ( +g ` (/) ) x ) = x /\ ( x ( +g ` (/) ) e ) = x ) )
7 6 nex 
 |-  -. E. e ( e e. (/) /\ A. x e. (/) ( ( e ( +g ` (/) ) x ) = x /\ ( x ( +g ` (/) ) e ) = x ) )
8 euex 
 |-  ( E! e ( e e. (/) /\ A. x e. (/) ( ( e ( +g ` (/) ) x ) = x /\ ( x ( +g ` (/) ) e ) = x ) ) -> E. e ( e e. (/) /\ A. x e. (/) ( ( e ( +g ` (/) ) x ) = x /\ ( x ( +g ` (/) ) e ) = x ) ) )
9 7 8 mto 
 |-  -. E! e ( e e. (/) /\ A. x e. (/) ( ( e ( +g ` (/) ) x ) = x /\ ( x ( +g ` (/) ) e ) = x ) )
10 iotanul 
 |-  ( -. E! e ( e e. (/) /\ A. x e. (/) ( ( e ( +g ` (/) ) x ) = x /\ ( x ( +g ` (/) ) e ) = x ) ) -> ( iota e ( e e. (/) /\ A. x e. (/) ( ( e ( +g ` (/) ) x ) = x /\ ( x ( +g ` (/) ) e ) = x ) ) ) = (/) )
11 9 10 ax-mp 
 |-  ( iota e ( e e. (/) /\ A. x e. (/) ( ( e ( +g ` (/) ) x ) = x /\ ( x ( +g ` (/) ) e ) = x ) ) ) = (/)
12 4 11 eqtr2i 
 |-  (/) = ( 0g ` (/) )