issubrng

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

		Ref	Expression
	Hypothesis	issubrng.b	$⊢ B = {Base}_{R}$
	Assertion	issubrng	Could not format assertion : No typesetting found for \|- ( A e. ( SubRng ` R ) <-> ( R e. Rng /\ ( R \|`s A ) e. Rng /\ A C_ B ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		issubrng.b	$⊢ B = {Base}_{R}$
2		df-subrng	Could not format SubRng = ( w e. Rng \|-> { s e. ~P ( Base ` w ) \| ( w \|`s s ) e. Rng } ) : No typesetting found for \|- SubRng = ( w e. Rng \|-> { s e. ~P ( Base ` w ) \| ( w \|`s s ) e. Rng } ) with typecode \|-
3	2	mptrcl	Could not format ( A e. ( SubRng ` R ) -> R e. Rng ) : No typesetting found for \|- ( A e. ( SubRng ` R ) -> R e. Rng ) with typecode \|-
4		simp1	$⊢ (R \in Rng \land R ↾_{𝑠} A \in Rng \land A \subseteq B) \to R \in Rng$
5		fveq2	$⊢ r = R \to {Base}_{r} = {Base}_{R}$
6	5	pweqd	$⊢ r = R \to 𝒫 {Base}_{r} = 𝒫 {Base}_{R}$
7		oveq1	$⊢ r = R \to r ↾_{𝑠} s = R ↾_{𝑠} s$
8	7	eleq1d	$⊢ r = R \to (r ↾_{𝑠} s \in Rng \leftrightarrow R ↾_{𝑠} s \in Rng)$
9	6 8	rabeqbidv	$⊢ r = R \to \{s \in 𝒫 {Base}_{r} \| r ↾_{𝑠} s \in Rng\} = \{s \in 𝒫 {Base}_{R} \| R ↾_{𝑠} s \in Rng\}$
10		df-subrng	Could not format SubRng = ( r e. Rng \|-> { s e. ~P ( Base ` r ) \| ( r \|`s s ) e. Rng } ) : No typesetting found for \|- SubRng = ( r e. Rng \|-> { s e. ~P ( Base ` r ) \| ( r \|`s s ) e. Rng } ) with typecode \|-
11		fvex	$⊢ {Base}_{R} \in V$
12	11	pwex	$⊢ 𝒫 {Base}_{R} \in V$
13	12	rabex	$⊢ \{s \in 𝒫 {Base}_{R} \| R ↾_{𝑠} s \in Rng\} \in V$
14	9 10 13	fvmpt	Could not format ( R e. Rng -> ( SubRng ` R ) = { s e. ~P ( Base ` R ) \| ( R \|`s s ) e. Rng } ) : No typesetting found for \|- ( R e. Rng -> ( SubRng ` R ) = { s e. ~P ( Base ` R ) \| ( R \|`s s ) e. Rng } ) with typecode \|-
15	14	eleq2d	Could not format ( R e. Rng -> ( A e. ( SubRng ` R ) <-> A e. { s e. ~P ( Base ` R ) \| ( R \|`s s ) e. Rng } ) ) : No typesetting found for \|- ( R e. Rng -> ( A e. ( SubRng ` R ) <-> A e. { s e. ~P ( Base ` R ) \| ( R \|`s s ) e. Rng } ) ) with typecode \|-
16		oveq2	$⊢ s = A \to R ↾_{𝑠} s = R ↾_{𝑠} A$
17	16	eleq1d	$⊢ s = A \to (R ↾_{𝑠} s \in Rng \leftrightarrow R ↾_{𝑠} A \in Rng)$
18	17	elrab	$⊢ A \in \{s \in 𝒫 {Base}_{R} \| R ↾_{𝑠} s \in Rng\} \leftrightarrow (A \in 𝒫 {Base}_{R} \land R ↾_{𝑠} A \in Rng)$
19	1	eqcomi	$⊢ {Base}_{R} = B$
20	19	sseq2i	$⊢ A \subseteq {Base}_{R} \leftrightarrow A \subseteq B$
21	20	anbi2i	$⊢ (R ↾_{𝑠} A \in Rng \land A \subseteq {Base}_{R}) \leftrightarrow (R ↾_{𝑠} A \in Rng \land A \subseteq B)$
22		ibar	$⊢ R \in Rng \to ((R ↾_{𝑠} A \in Rng \land A \subseteq B) \leftrightarrow (R \in Rng \land (R ↾_{𝑠} A \in Rng \land A \subseteq B)))$
23	21 22	bitrid	$⊢ R \in Rng \to ((R ↾_{𝑠} A \in Rng \land A \subseteq {Base}_{R}) \leftrightarrow (R \in Rng \land (R ↾_{𝑠} A \in Rng \land A \subseteq B)))$
24	11	elpw2	$⊢ A \in 𝒫 {Base}_{R} \leftrightarrow A \subseteq {Base}_{R}$
25	24	anbi2ci	$⊢ (A \in 𝒫 {Base}_{R} \land R ↾_{𝑠} A \in Rng) \leftrightarrow (R ↾_{𝑠} A \in Rng \land A \subseteq {Base}_{R})$
26		3anass	$⊢ (R \in Rng \land R ↾_{𝑠} A \in Rng \land A \subseteq B) \leftrightarrow (R \in Rng \land (R ↾_{𝑠} A \in Rng \land A \subseteq B))$
27	23 25 26	3bitr4g	$⊢ R \in Rng \to ((A \in 𝒫 {Base}_{R} \land R ↾_{𝑠} A \in Rng) \leftrightarrow (R \in Rng \land R ↾_{𝑠} A \in Rng \land A \subseteq B))$
28	18 27	bitrid	$⊢ R \in Rng \to (A \in \{s \in 𝒫 {Base}_{R} \| R ↾_{𝑠} s \in Rng\} \leftrightarrow (R \in Rng \land R ↾_{𝑠} A \in Rng \land A \subseteq B))$
29	15 28	bitrd	Could not format ( R e. Rng -> ( A e. ( SubRng ` R ) <-> ( R e. Rng /\ ( R \|`s A ) e. Rng /\ A C_ B ) ) ) : No typesetting found for \|- ( R e. Rng -> ( A e. ( SubRng ` R ) <-> ( R e. Rng /\ ( R \|`s A ) e. Rng /\ A C_ B ) ) ) with typecode \|-
30	3 4 29	pm5.21nii	Could not format ( A e. ( SubRng ` R ) <-> ( R e. Rng /\ ( R \|`s A ) e. Rng /\ A C_ B ) ) : No typesetting found for \|- ( A e. ( SubRng ` R ) <-> ( R e. Rng /\ ( R \|`s A ) e. Rng /\ A C_ B ) ) with typecode \|-

Metamath Proof Explorer

Theorem issubrng

Proof