Description: The category of rings is a category. (Contributed by AV, 14-Feb-2020) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ringccatALTV.c | ⊢ 𝐶 = ( RingCatALTV ‘ 𝑈 ) | |
Assertion | ringccatALTV | ⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ Cat ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ringccatALTV.c | ⊢ 𝐶 = ( RingCatALTV ‘ 𝑈 ) | |
2 | eqid | ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 ) | |
3 | 1 2 | ringccatidALTV | ⊢ ( 𝑈 ∈ 𝑉 → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( I ↾ ( Base ‘ 𝑥 ) ) ) ) ) |
4 | 3 | simpld | ⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ Cat ) |