This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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