Theorem issubrng

Description: The subring of non-unital ring predicate. (Contributed by AV, 14-Feb-2025)

	Ref	Expression
Hypothesis	issubrng.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion	issubrng	⊢ ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ↔ ( 𝑅 ∈ Rng ∧ ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		issubrng.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		df-subrng	⊢ SubRng = ( 𝑤 ∈ Rng ↦ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ ( 𝑤 ↾s 𝑠 ) ∈ Rng } )
3	2	mptrcl	⊢ ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) → 𝑅 ∈ Rng )
4		simp1	⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ 𝐵 ) → 𝑅 ∈ Rng )
5		fveq2	⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
6	5	pweqd	⊢ ( 𝑟 = 𝑅 → 𝒫 ( Base ‘ 𝑟 ) = 𝒫 ( Base ‘ 𝑅 ) )
7		oveq1	⊢ ( 𝑟 = 𝑅 → ( 𝑟 ↾s 𝑠 ) = ( 𝑅 ↾s 𝑠 ) )
8	7	eleq1d	⊢ ( 𝑟 = 𝑅 → ( ( 𝑟 ↾s 𝑠 ) ∈ Rng ↔ ( 𝑅 ↾s 𝑠 ) ∈ Rng ) )
9	6 8	rabeqbidv	⊢ ( 𝑟 = 𝑅 → { 𝑠 ∈ 𝒫 ( Base ‘ 𝑟 ) ∣ ( 𝑟 ↾s 𝑠 ) ∈ Rng } = { 𝑠 ∈ 𝒫 ( Base ‘ 𝑅 ) ∣ ( 𝑅 ↾s 𝑠 ) ∈ Rng } )
10		df-subrng	⊢ SubRng = ( 𝑟 ∈ Rng ↦ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑟 ) ∣ ( 𝑟 ↾s 𝑠 ) ∈ Rng } )
11		fvex	⊢ ( Base ‘ 𝑅 ) ∈ V
12	11	pwex	⊢ 𝒫 ( Base ‘ 𝑅 ) ∈ V
13	12	rabex	⊢ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑅 ) ∣ ( 𝑅 ↾s 𝑠 ) ∈ Rng } ∈ V
14	9 10 13	fvmpt	⊢ ( 𝑅 ∈ Rng → ( SubRng ‘ 𝑅 ) = { 𝑠 ∈ 𝒫 ( Base ‘ 𝑅 ) ∣ ( 𝑅 ↾s 𝑠 ) ∈ Rng } )
15	14	eleq2d	⊢ ( 𝑅 ∈ Rng → ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ↔ 𝐴 ∈ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑅 ) ∣ ( 𝑅 ↾s 𝑠 ) ∈ Rng } ) )
16		oveq2	⊢ ( 𝑠 = 𝐴 → ( 𝑅 ↾s 𝑠 ) = ( 𝑅 ↾s 𝐴 ) )
17	16	eleq1d	⊢ ( 𝑠 = 𝐴 → ( ( 𝑅 ↾s 𝑠 ) ∈ Rng ↔ ( 𝑅 ↾s 𝐴 ) ∈ Rng ) )
18	17	elrab	⊢ ( 𝐴 ∈ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑅 ) ∣ ( 𝑅 ↾s 𝑠 ) ∈ Rng } ↔ ( 𝐴 ∈ 𝒫 ( Base ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝐴 ) ∈ Rng ) )
19	1	eqcomi	⊢ ( Base ‘ 𝑅 ) = 𝐵
20	19	sseq2i	⊢ ( 𝐴 ⊆ ( Base ‘ 𝑅 ) ↔ 𝐴 ⊆ 𝐵 )
21	20	anbi2i	⊢ ( ( ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ ( Base ‘ 𝑅 ) ) ↔ ( ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ 𝐵 ) )
22		ibar	⊢ ( 𝑅 ∈ Rng → ( ( ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ 𝐵 ) ↔ ( 𝑅 ∈ Rng ∧ ( ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ 𝐵 ) ) ) )
23	21 22	bitrid	⊢ ( 𝑅 ∈ Rng → ( ( ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ ( Base ‘ 𝑅 ) ) ↔ ( 𝑅 ∈ Rng ∧ ( ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ 𝐵 ) ) ) )
24	11	elpw2	⊢ ( 𝐴 ∈ 𝒫 ( Base ‘ 𝑅 ) ↔ 𝐴 ⊆ ( Base ‘ 𝑅 ) )
25	24	anbi2ci	⊢ ( ( 𝐴 ∈ 𝒫 ( Base ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝐴 ) ∈ Rng ) ↔ ( ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ ( Base ‘ 𝑅 ) ) )
26		3anass	⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ 𝐵 ) ↔ ( 𝑅 ∈ Rng ∧ ( ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ 𝐵 ) ) )
27	23 25 26	3bitr4g	⊢ ( 𝑅 ∈ Rng → ( ( 𝐴 ∈ 𝒫 ( Base ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝐴 ) ∈ Rng ) ↔ ( 𝑅 ∈ Rng ∧ ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ 𝐵 ) ) )
28	18 27	bitrid	⊢ ( 𝑅 ∈ Rng → ( 𝐴 ∈ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑅 ) ∣ ( 𝑅 ↾s 𝑠 ) ∈ Rng } ↔ ( 𝑅 ∈ Rng ∧ ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ 𝐵 ) ) )
29	15 28	bitrd	⊢ ( 𝑅 ∈ Rng → ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ↔ ( 𝑅 ∈ Rng ∧ ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ 𝐵 ) ) )
30	3 4 29	pm5.21nii	⊢ ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ↔ ( 𝑅 ∈ Rng ∧ ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ 𝐵 ) )