Metamath Proof Explorer

Theorem refrelsredund4

Description: The naive version of the class of reflexive relations is redundant with respect to the class of reflexive relations (see dfrefrels2 ) if the relations are symmetric as well. (Contributed by Peter Mazsa, 26-Oct-2022)

Ref Expression
Assertion refrelsredund4 
|- { r e. Rels | ( _I |` dom r ) C_ r } Redund <. RefRels , ( RefRels i^i SymRels ) >.

Proof

Step Hyp Ref Expression
1 inxpssres 
 |-  ( _I i^i ( dom r X. ran r ) ) C_ ( _I |` dom r )
2 sstr2 
 |-  ( ( _I i^i ( dom r X. ran r ) ) C_ ( _I |` dom r ) -> ( ( _I |` dom r ) C_ r -> ( _I i^i ( dom r X. ran r ) ) C_ r ) )
3 1 2 ax-mp 
 |-  ( ( _I |` dom r ) C_ r -> ( _I i^i ( dom r X. ran r ) ) C_ r )
4 3 ssrabi 
 |-  { r e. Rels | ( _I |` dom r ) C_ r } C_ { r e. Rels | ( _I i^i ( dom r X. ran r ) ) C_ r }
5 dfrefrels2 
 |-  RefRels = { r e. Rels | ( _I i^i ( dom r X. ran r ) ) C_ r }
6 4 5 sseqtrri 
 |-  { r e. Rels | ( _I |` dom r ) C_ r } C_ RefRels
7 in32 
 |-  ( ( { r e. Rels | ( _I |` dom r ) C_ r } i^i SymRels ) i^i RefRels ) = ( ( { r e. Rels | ( _I |` dom r ) C_ r } i^i RefRels ) i^i SymRels )
8 inrab 
 |-  ( { r e. Rels | ( _I |` dom r ) C_ r } i^i { r e. Rels | `' r C_ r } ) = { r e. Rels | ( ( _I |` dom r ) C_ r /\ `' r C_ r ) }
9 dfsymrels2 
 |-  SymRels = { r e. Rels | `' r C_ r }
10 9 ineq2i 
 |-  ( { r e. Rels | ( _I |` dom r ) C_ r } i^i SymRels ) = ( { r e. Rels | ( _I |` dom r ) C_ r } i^i { r e. Rels | `' r C_ r } )
11 refsymrels2 
 |-  ( RefRels i^i SymRels ) = { r e. Rels | ( ( _I |` dom r ) C_ r /\ `' r C_ r ) }
12 8 10 11 3eqtr4i 
 |-  ( { r e. Rels | ( _I |` dom r ) C_ r } i^i SymRels ) = ( RefRels i^i SymRels )
13 12 ineq1i 
 |-  ( ( { r e. Rels | ( _I |` dom r ) C_ r } i^i SymRels ) i^i RefRels ) = ( ( RefRels i^i SymRels ) i^i RefRels )
14 inass 
 |-  ( ( { r e. Rels | ( _I |` dom r ) C_ r } i^i RefRels ) i^i SymRels ) = ( { r e. Rels | ( _I |` dom r ) C_ r } i^i ( RefRels i^i SymRels ) )
15 7 13 14 3eqtr3ri 
 |-  ( { r e. Rels | ( _I |` dom r ) C_ r } i^i ( RefRels i^i SymRels ) ) = ( ( RefRels i^i SymRels ) i^i RefRels )
16 in32 
 |-  ( ( RefRels i^i SymRels ) i^i RefRels ) = ( ( RefRels i^i RefRels ) i^i SymRels )
17 inass 
 |-  ( ( RefRels i^i RefRels ) i^i SymRels ) = ( RefRels i^i ( RefRels i^i SymRels ) )
18 15 16 17 3eqtri 
 |-  ( { r e. Rels | ( _I |` dom r ) C_ r } i^i ( RefRels i^i SymRels ) ) = ( RefRels i^i ( RefRels i^i SymRels ) )
19 df-redund 
 |-  ( { r e. Rels | ( _I |` dom r ) C_ r } Redund <. RefRels , ( RefRels i^i SymRels ) >. <-> ( { r e. Rels | ( _I |` dom r ) C_ r } C_ RefRels /\ ( { r e. Rels | ( _I |` dom r ) C_ r } i^i ( RefRels i^i SymRels ) ) = ( RefRels i^i ( RefRels i^i SymRels ) ) ) )
20 6 18 19 mpbir2an 
 |-  { r e. Rels | ( _I |` dom r ) C_ r } Redund <. RefRels , ( RefRels i^i SymRels ) >.