Metamath Proof Explorer
Description: The group zero extractor is a function. (Contributed by Stefan O'Rear, 10-Jan-2015)
|
|
Ref |
Expression |
|
Assertion |
fn0g |
⊢ 0g Fn V |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
iotaex |
⊢ ( ℩ 𝑒 ( 𝑒 ∈ ( Base ‘ 𝑔 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( ( 𝑒 ( +g ‘ 𝑔 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝑔 ) 𝑒 ) = 𝑥 ) ) ) ∈ V |
2 |
|
df-0g |
⊢ 0g = ( 𝑔 ∈ V ↦ ( ℩ 𝑒 ( 𝑒 ∈ ( Base ‘ 𝑔 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( ( 𝑒 ( +g ‘ 𝑔 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝑔 ) 𝑒 ) = 𝑥 ) ) ) ) |
3 |
1 2
|
fnmpti |
⊢ 0g Fn V |