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

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 ⊢ ⊕ ˙ ∈ G GrpAct Y → Y ∈ V

Proof

Step Hyp Ref Expression
1 eqid ⊢ Base G = Base G
2 eqid ⊢ + G = + G
3 eqid ⊢ 0 G = 0 G
4 1 2 3 isga ⊢ ⊕ ˙ ∈ G GrpAct Y ↔ G ∈ Grp ∧ Y ∈ V ∧ ⊕ ˙ : Base G × Y ⟶ Y ∧ ∀ x ∈ Y 0 G ⊕ ˙ x = x ∧ ∀ y ∈ Base G ∀ z ∈ Base G y + G z ⊕ ˙ x = y ⊕ ˙ z ⊕ ˙ x
5 4 simplbi ⊢ ⊕ ˙ ∈ G GrpAct Y → G ∈ Grp ∧ Y ∈ V
6 5 simprd ⊢ ⊕ ˙ ∈ G GrpAct Y → Y ∈ V