Metamath Proof Explorer

Theorem gaset

Description: The right argument of a group action is a set. (Contributed by Mario Carneiro, 30-Apr-2015)

Ref Expression
Assertion gaset 
|- ( .(+) e. ( G GrpAct Y ) -> Y e. _V )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` G ) = ( Base ` G )
2 eqid 
 |-  ( +g ` G ) = ( +g ` G )
3 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
4 1 2 3 isga 
 |-  ( .(+) e. ( G GrpAct Y ) <-> ( ( G e. Grp /\ Y e. _V ) /\ ( .(+) : ( ( Base ` G ) X. Y ) --> Y /\ A. x e. Y ( ( ( 0g ` G ) .(+) x ) = x /\ A. y e. ( Base ` G ) A. z e. ( Base ` G ) ( ( y ( +g ` G ) z ) .(+) x ) = ( y .(+) ( z .(+) x ) ) ) ) ) )
5 4 simplbi 
 |-  ( .(+) e. ( G GrpAct Y ) -> ( G e. Grp /\ Y e. _V ) )
6 5 simprd 
 |-  ( .(+) e. ( G GrpAct Y ) -> Y e. _V )