Theorem gafo

Description: A group action is onto its base set. (Contributed by Jeff Hankins, 10-Aug-2009) (Revised by Mario Carneiro, 13-Jan-2015)

	Ref	Expression
Hypothesis	gaf.1	|- X = ( Base ` G )
Assertion	gafo	|- ( .(+) e. ( G GrpAct Y ) -> .(+) : ( X X. Y ) -onto-> Y )

Proof

Step	Hyp	Ref	Expression
1		gaf.1	|- X = ( Base ` G )
2	1	gaf	|- ( .(+) e. ( G GrpAct Y ) -> .(+) : ( X X. Y ) --> Y )
3		gagrp	|- ( .(+) e. ( G GrpAct Y ) -> G e. Grp )
4	3	adantr	|- ( ( .(+) e. ( G GrpAct Y ) /\ x e. Y ) -> G e. Grp )
5		eqid	|- ( 0g ` G ) = ( 0g ` G )
6	1 5	grpidcl	|- ( G e. Grp -> ( 0g ` G ) e. X )
7	4 6	syl	|- ( ( .(+) e. ( G GrpAct Y ) /\ x e. Y ) -> ( 0g ` G ) e. X )
8		simpr	|- ( ( .(+) e. ( G GrpAct Y ) /\ x e. Y ) -> x e. Y )
9	5	gagrpid	|- ( ( .(+) e. ( G GrpAct Y ) /\ x e. Y ) -> ( ( 0g ` G ) .(+) x ) = x )
10	9	eqcomd	|- ( ( .(+) e. ( G GrpAct Y ) /\ x e. Y ) -> x = ( ( 0g ` G ) .(+) x ) )
11		rspceov	|- ( ( ( 0g ` G ) e. X /\ x e. Y /\ x = ( ( 0g ` G ) .(+) x ) ) -> E. y e. X E. z e. Y x = ( y .(+) z ) )
12	7 8 10 11	syl3anc	|- ( ( .(+) e. ( G GrpAct Y ) /\ x e. Y ) -> E. y e. X E. z e. Y x = ( y .(+) z ) )
13	12	ralrimiva	|- ( .(+) e. ( G GrpAct Y ) -> A. x e. Y E. y e. X E. z e. Y x = ( y .(+) z ) )
14		foov	|- ( .(+) : ( X X. Y ) -onto-> Y <-> ( .(+) : ( X X. Y ) --> Y /\ A. x e. Y E. y e. X E. z e. Y x = ( y .(+) z ) ) )
15	2 13 14	sylanbrc	|- ( .(+) e. ( G GrpAct Y ) -> .(+) : ( X X. Y ) -onto-> Y )