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 { 𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟 ) ⊆ 𝑟 } Redund ⟨ RefRels , ( RefRels ∩ SymRels ) ⟩

Proof

Step Hyp Ref Expression
1 inxpssres ⊢ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ ( I ↾ dom 𝑟 )
2 sstr2 ⊢ ( ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ ( I ↾ dom 𝑟 ) → ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 → ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ 𝑟 ) )
3 1 2 ax-mp ⊢ ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 → ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ 𝑟 )
4 3 ssrabi ⊢ { 𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟 ) ⊆ 𝑟 } ⊆ { 𝑟 ∈ Rels ∣ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ 𝑟 }
5 dfrefrels2 ⊢ RefRels = { 𝑟 ∈ Rels ∣ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ 𝑟 }
6 4 5 sseqtrri ⊢ { 𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟 ) ⊆ 𝑟 } ⊆ RefRels
7 in32 ⊢ ( ( { 𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟 ) ⊆ 𝑟 } ∩ SymRels ) ∩ RefRels ) = ( ( { 𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟 ) ⊆ 𝑟 } ∩ RefRels ) ∩ SymRels )
8 inrab ⊢ ( { 𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟 ) ⊆ 𝑟 } ∩ { 𝑟 ∈ Rels ∣ ◡ 𝑟 ⊆ 𝑟 } ) = { 𝑟 ∈ Rels ∣ ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ ◡ 𝑟 ⊆ 𝑟 ) }
9 dfsymrels2 ⊢ SymRels = { 𝑟 ∈ Rels ∣ ◡ 𝑟 ⊆ 𝑟 }
10 9 ineq2i ⊢ ( { 𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟 ) ⊆ 𝑟 } ∩ SymRels ) = ( { 𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟 ) ⊆ 𝑟 } ∩ { 𝑟 ∈ Rels ∣ ◡ 𝑟 ⊆ 𝑟 } )
11 refsymrels2 ⊢ ( RefRels ∩ SymRels ) = { 𝑟 ∈ Rels ∣ ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ ◡ 𝑟 ⊆ 𝑟 ) }
12 8 10 11 3eqtr4i ⊢ ( { 𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟 ) ⊆ 𝑟 } ∩ SymRels ) = ( RefRels ∩ SymRels )
13 12 ineq1i ⊢ ( ( { 𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟 ) ⊆ 𝑟 } ∩ SymRels ) ∩ RefRels ) = ( ( RefRels ∩ SymRels ) ∩ RefRels )
14 inass ⊢ ( ( { 𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟 ) ⊆ 𝑟 } ∩ RefRels ) ∩ SymRels ) = ( { 𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟 ) ⊆ 𝑟 } ∩ ( RefRels ∩ SymRels ) )
15 7 13 14 3eqtr3ri ⊢ ( { 𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟 ) ⊆ 𝑟 } ∩ ( RefRels ∩ SymRels ) ) = ( ( RefRels ∩ SymRels ) ∩ RefRels )
16 in32 ⊢ ( ( RefRels ∩ SymRels ) ∩ RefRels ) = ( ( RefRels ∩ RefRels ) ∩ SymRels )
17 inass ⊢ ( ( RefRels ∩ RefRels ) ∩ SymRels ) = ( RefRels ∩ ( RefRels ∩ SymRels ) )
18 15 16 17 3eqtri ⊢ ( { 𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟 ) ⊆ 𝑟 } ∩ ( RefRels ∩ SymRels ) ) = ( RefRels ∩ ( RefRels ∩ SymRels ) )
19 df-redund ⊢ ( { 𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟 ) ⊆ 𝑟 } Redund ⟨ RefRels , ( RefRels ∩ SymRels ) ⟩ ↔ ( { 𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟 ) ⊆ 𝑟 } ⊆ RefRels ∧ ( { 𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟 ) ⊆ 𝑟 } ∩ ( RefRels ∩ SymRels ) ) = ( RefRels ∩ ( RefRels ∩ SymRels ) ) ) )
20 6 18 19 mpbir2an ⊢ { 𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟 ) ⊆ 𝑟 } Redund ⟨ RefRels , ( RefRels ∩ SymRels ) ⟩