df-subrng

Description: Define a subring of a non-unital ring as a set of elements that is a non-unital ring in its own right. In this section, a subring of a non-unital ring is simply called "subring", unless it causes any ambiguity with SubRing . (Contributed by AV, 14-Feb-2025)

		Ref	Expression
	Assertion	df-subrng	⊢ SubRng = ( 𝑤 ∈ Rng ↦ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ ( 𝑤 ↾_s 𝑠 ) ∈ Rng } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csubrng	⊢ SubRng
1		vw	⊢ 𝑤
2		crng	⊢ Rng
3		vs	⊢ 𝑠
4		cbs	⊢ Base
5	1	cv	⊢ 𝑤
6	5 4	cfv	⊢ ( Base ‘ 𝑤 )
7	6	cpw	⊢ 𝒫 ( Base ‘ 𝑤 )
8		cress	⊢ ↾_s
9	3	cv	⊢ 𝑠
10	5 9 8	co	⊢ ( 𝑤 ↾_s 𝑠 )
11	10 2	wcel	⊢ ( 𝑤 ↾_s 𝑠 ) ∈ Rng
12	11 3 7	crab	⊢ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ ( 𝑤 ↾_s 𝑠 ) ∈ Rng }
13	1 2 12	cmpt	⊢ ( 𝑤 ∈ Rng ↦ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ ( 𝑤 ↾_s 𝑠 ) ∈ Rng } )
14	0 13	wceq	⊢ SubRng = ( 𝑤 ∈ Rng ↦ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ ( 𝑤 ↾_s 𝑠 ) ∈ Rng } )

Metamath Proof Explorer

Definition df-subrng

Detailed syntax breakdown