Step |
Hyp |
Ref |
Expression |
1 |
|
vex |
⊢ 𝑧 ∈ V |
2 |
|
eqid |
⊢ { ⟨ ( Base ‘ ndx ) , { 𝑧 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ } = { ⟨ ( Base ‘ ndx ) , { 𝑧 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ } |
3 |
2
|
ring1 |
⊢ ( 𝑧 ∈ V → { ⟨ ( Base ‘ ndx ) , { 𝑧 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ } ∈ Ring ) |
4 |
|
ne0i |
⊢ ( { ⟨ ( Base ‘ ndx ) , { 𝑧 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ } ∈ Ring → Ring ≠ ∅ ) |
5 |
1 3 4
|
mp2b |
⊢ Ring ≠ ∅ |