Description: Abelian groups (and therefore also groups and monoids) exist. (Contributed by AV, 29-Apr-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | abln0 | ⊢ Abel ≠ ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex | ⊢ 𝑖 ∈ V | |
2 | eqid | ⊢ { 〈 ( Base ‘ ndx ) , { 𝑖 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑖 , 𝑖 〉 , 𝑖 〉 } 〉 } = { 〈 ( Base ‘ ndx ) , { 𝑖 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑖 , 𝑖 〉 , 𝑖 〉 } 〉 } | |
3 | 2 | abl1 | ⊢ ( 𝑖 ∈ V → { 〈 ( Base ‘ ndx ) , { 𝑖 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑖 , 𝑖 〉 , 𝑖 〉 } 〉 } ∈ Abel ) |
4 | ne0i | ⊢ ( { 〈 ( Base ‘ ndx ) , { 𝑖 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑖 , 𝑖 〉 , 𝑖 〉 } 〉 } ∈ Abel → Abel ≠ ∅ ) | |
5 | 1 3 4 | mp2b | ⊢ Abel ≠ ∅ |