Metamath Proof Explorer


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 ˙ G GrpAct Y ˙ : X × Y onto Y

Proof

Step Hyp Ref Expression
1 gaf.1 X = Base G
2 1 gaf ˙ G GrpAct Y ˙ : X × Y Y
3 gagrp ˙ G GrpAct Y G Grp
4 3 adantr ˙ G GrpAct Y x Y G Grp
5 eqid 0 G = 0 G
6 1 5 grpidcl G Grp 0 G X
7 4 6 syl ˙ G GrpAct Y x Y 0 G X
8 simpr ˙ G GrpAct Y x Y x Y
9 5 gagrpid ˙ G GrpAct Y x Y 0 G ˙ x = x
10 9 eqcomd ˙ G GrpAct Y x Y x = 0 G ˙ x
11 rspceov 0 G X x Y x = 0 G ˙ x y X z Y x = y ˙ z
12 7 8 10 11 syl3anc ˙ G GrpAct Y x Y y X z Y x = y ˙ z
13 12 ralrimiva ˙ G GrpAct Y x Y y X z Y x = y ˙ z
14 foov ˙ : X × Y onto Y ˙ : X × Y Y x Y y X z Y x = y ˙ z
15 2 13 14 sylanbrc ˙ G GrpAct Y ˙ : X × Y onto Y