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 ( ∈ ( 𝐺 GrpAct 𝑌 ) → 𝑌 ∈ V )

Proof

Step Hyp Ref Expression
1 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
2 eqid ( +g𝐺 ) = ( +g𝐺 )
3 eqid ( 0g𝐺 ) = ( 0g𝐺 )
4 1 2 3 isga ( ∈ ( 𝐺 GrpAct 𝑌 ) ↔ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ V ) ∧ ( : ( ( Base ‘ 𝐺 ) × 𝑌 ) ⟶ 𝑌 ∧ ∀ 𝑥𝑌 ( ( ( 0g𝐺 ) 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( ( 𝑦 ( +g𝐺 ) 𝑧 ) 𝑥 ) = ( 𝑦 ( 𝑧 𝑥 ) ) ) ) ) )
5 4 simplbi ( ∈ ( 𝐺 GrpAct 𝑌 ) → ( 𝐺 ∈ Grp ∧ 𝑌 ∈ V ) )
6 5 simprd ( ∈ ( 𝐺 GrpAct 𝑌 ) → 𝑌 ∈ V )