Description: The right argument of a group action is a set. (Contributed by Mario Carneiro, 30-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | gaset | ⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → 𝑌 ∈ V ) |
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 ) |