Metamath Proof Explorer

Theorem 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 
|- ( A e. ( SubRng ` R ) <-> ( R e. Rng /\ ( R |`s A ) e. Rng /\ A C_ B ) )

Proof

Step Hyp Ref Expression
1 issubrng.b 
 |-  B = ( Base ` R )
2 df-subrng 
 |-  SubRng = ( w e. Rng |-> { s e. ~P ( Base ` w ) | ( w |`s s ) e. Rng } )
3 2 mptrcl 
 |-  ( A e. ( SubRng ` R ) -> R e. Rng )
4 simp1 
 |-  ( ( R e. Rng /\ ( R |`s A ) e. Rng /\ A C_ B ) -> R e. Rng )
5 fveq2 
 |-  ( r = R -> ( Base ` r ) = ( Base ` R ) )
6 5 pweqd 
 |-  ( r = R -> ~P ( Base ` r ) = ~P ( Base ` R ) )
7 oveq1 
 |-  ( r = R -> ( r |`s s ) = ( R |`s s ) )
8 7 eleq1d 
 |-  ( r = R -> ( ( r |`s s ) e. Rng <-> ( R |`s s ) e. Rng ) )
9 6 8 rabeqbidv 
 |-  ( r = R -> { s e. ~P ( Base ` r ) | ( r |`s s ) e. Rng } = { s e. ~P ( Base ` R ) | ( R |`s s ) e. Rng } )
10 df-subrng 
 |-  SubRng = ( r e. Rng |-> { s e. ~P ( Base ` r ) | ( r |`s s ) e. Rng } )
11 fvex 
 |-  ( Base ` R ) e. _V
12 11 pwex 
 |-  ~P ( Base ` R ) e. _V
13 12 rabex 
 |-  { s e. ~P ( Base ` R ) | ( R |`s s ) e. Rng } e. _V
14 9 10 13 fvmpt 
 |-  ( R e. Rng -> ( SubRng ` R ) = { s e. ~P ( Base ` R ) | ( R |`s s ) e. Rng } )
15 14 eleq2d 
 |-  ( R e. Rng -> ( A e. ( SubRng ` R ) <-> A e. { s e. ~P ( Base ` R ) | ( R |`s s ) e. Rng } ) )
16 oveq2 
 |-  ( s = A -> ( R |`s s ) = ( R |`s A ) )
17 16 eleq1d 
 |-  ( s = A -> ( ( R |`s s ) e. Rng <-> ( R |`s A ) e. Rng ) )
18 17 elrab 
 |-  ( A e. { s e. ~P ( Base ` R ) | ( R |`s s ) e. Rng } <-> ( A e. ~P ( Base ` R ) /\ ( R |`s A ) e. Rng ) )
19 1 eqcomi 
 |-  ( Base ` R ) = B
20 19 sseq2i 
 |-  ( A C_ ( Base ` R ) <-> A C_ B )
21 20 anbi2i 
 |-  ( ( ( R |`s A ) e. Rng /\ A C_ ( Base ` R ) ) <-> ( ( R |`s A ) e. Rng /\ A C_ B ) )
22 ibar 
 |-  ( R e. Rng -> ( ( ( R |`s A ) e. Rng /\ A C_ B ) <-> ( R e. Rng /\ ( ( R |`s A ) e. Rng /\ A C_ B ) ) ) )
23 21 22 bitrid 
 |-  ( R e. Rng -> ( ( ( R |`s A ) e. Rng /\ A C_ ( Base ` R ) ) <-> ( R e. Rng /\ ( ( R |`s A ) e. Rng /\ A C_ B ) ) ) )
24 11 elpw2 
 |-  ( A e. ~P ( Base ` R ) <-> A C_ ( Base ` R ) )
25 24 anbi2ci 
 |-  ( ( A e. ~P ( Base ` R ) /\ ( R |`s A ) e. Rng ) <-> ( ( R |`s A ) e. Rng /\ A C_ ( Base ` R ) ) )
26 3anass 
 |-  ( ( R e. Rng /\ ( R |`s A ) e. Rng /\ A C_ B ) <-> ( R e. Rng /\ ( ( R |`s A ) e. Rng /\ A C_ B ) ) )
27 23 25 26 3bitr4g 
 |-  ( R e. Rng -> ( ( A e. ~P ( Base ` R ) /\ ( R |`s A ) e. Rng ) <-> ( R e. Rng /\ ( R |`s A ) e. Rng /\ A C_ B ) ) )
28 18 27 bitrid 
 |-  ( R e. Rng -> ( A e. { s e. ~P ( Base ` R ) | ( R |`s s ) e. Rng } <-> ( R e. Rng /\ ( R |`s A ) e. Rng /\ A C_ B ) ) )
29 15 28 bitrd 
 |-  ( R e. Rng -> ( A e. ( SubRng ` R ) <-> ( R e. Rng /\ ( R |`s A ) e. Rng /\ A C_ B ) ) )
30 3 4 29 pm5.21nii 
 |-  ( A e. ( SubRng ` R ) <-> ( R e. Rng /\ ( R |`s A ) e. Rng /\ A C_ B ) )