Metamath Proof Explorer

Theorem refrelredund4

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

		Ref	Expression
	Assertion	refrelredund4	⊢ redund ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) , RefRel 𝑅 , ( RefRel 𝑅 ∧ SymRel 𝑅 ) )

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	anim1i	⊢ ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) → ( ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ 𝑅 ∧ Rel 𝑅 ) )
5		dfrefrel2	⊢ ( RefRel 𝑅 ↔ ( ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ 𝑅 ∧ Rel 𝑅 ) )
6	4 5	sylibr	⊢ ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) → RefRel 𝑅 )
7		an12	⊢ ( ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) ∧ ( RefRel 𝑅 ∧ SymRel 𝑅 ) ) ↔ ( RefRel 𝑅 ∧ ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) ∧ SymRel 𝑅 ) ) )
8		anandir	⊢ ( ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ ^◡ 𝑅 ⊆ 𝑅 ) ∧ Rel 𝑅 ) ↔ ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) ∧ ( ^◡ 𝑅 ⊆ 𝑅 ∧ Rel 𝑅 ) ) )
9		refsymrel2	⊢ ( ( RefRel 𝑅 ∧ SymRel 𝑅 ) ↔ ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ ^◡ 𝑅 ⊆ 𝑅 ) ∧ Rel 𝑅 ) )
10		dfsymrel2	⊢ ( SymRel 𝑅 ↔ ( ^◡ 𝑅 ⊆ 𝑅 ∧ Rel 𝑅 ) )
11	10	anbi2i	⊢ ( ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) ∧ SymRel 𝑅 ) ↔ ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) ∧ ( ^◡ 𝑅 ⊆ 𝑅 ∧ Rel 𝑅 ) ) )
12	8 9 11	3bitr4i	⊢ ( ( RefRel 𝑅 ∧ SymRel 𝑅 ) ↔ ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) ∧ SymRel 𝑅 ) )
13	12	anbi2i	⊢ ( ( RefRel 𝑅 ∧ ( RefRel 𝑅 ∧ SymRel 𝑅 ) ) ↔ ( RefRel 𝑅 ∧ ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) ∧ SymRel 𝑅 ) ) )
14	7 13	bitr4i	⊢ ( ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) ∧ ( RefRel 𝑅 ∧ SymRel 𝑅 ) ) ↔ ( RefRel 𝑅 ∧ ( RefRel 𝑅 ∧ SymRel 𝑅 ) ) )
15		df-redundp	⊢ ( redund ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) , RefRel 𝑅 , ( RefRel 𝑅 ∧ SymRel 𝑅 ) ) ↔ ( ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) → RefRel 𝑅 ) ∧ ( ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) ∧ ( RefRel 𝑅 ∧ SymRel 𝑅 ) ) ↔ ( RefRel 𝑅 ∧ ( RefRel 𝑅 ∧ SymRel 𝑅 ) ) ) ) )
16	6 14 15	mpbir2an	⊢ redund ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) , RefRel 𝑅 , ( RefRel 𝑅 ∧ SymRel 𝑅 ) )