Theorem refsymrel2

Description: A relation which is reflexive and symmetric (like an equivalence relation) can use the restricted version for their reflexive part (see below), not just the (I i^i ( dom R X. ran R ) ) C R version of dfrefrel2 , cf. the comment of dfrefrels2 . (Contributed by Peter Mazsa, 23-Aug-2021)

	Ref	Expression
Assertion	refsymrel2	⊢ ( ( RefRel 𝑅 ∧ SymRel 𝑅 ) ↔ ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ ◡ 𝑅 ⊆ 𝑅 ) ∧ Rel 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		dfrefrel2	⊢ ( RefRel 𝑅 ↔ ( ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ 𝑅 ∧ Rel 𝑅 ) )
2		dfsymrel2	⊢ ( SymRel 𝑅 ↔ ( ◡ 𝑅 ⊆ 𝑅 ∧ Rel 𝑅 ) )
3	1 2	anbi12i	⊢ ( ( RefRel 𝑅 ∧ SymRel 𝑅 ) ↔ ( ( ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ 𝑅 ∧ Rel 𝑅 ) ∧ ( ◡ 𝑅 ⊆ 𝑅 ∧ Rel 𝑅 ) ) )
4		anandi3r	⊢ ( ( ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ 𝑅 ∧ Rel 𝑅 ∧ ◡ 𝑅 ⊆ 𝑅 ) ↔ ( ( ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ 𝑅 ∧ Rel 𝑅 ) ∧ ( ◡ 𝑅 ⊆ 𝑅 ∧ Rel 𝑅 ) ) )
5		3anan32	⊢ ( ( ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ 𝑅 ∧ Rel 𝑅 ∧ ◡ 𝑅 ⊆ 𝑅 ) ↔ ( ( ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ 𝑅 ∧ ◡ 𝑅 ⊆ 𝑅 ) ∧ Rel 𝑅 ) )
6	3 4 5	3bitr2i	⊢ ( ( RefRel 𝑅 ∧ SymRel 𝑅 ) ↔ ( ( ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ 𝑅 ∧ ◡ 𝑅 ⊆ 𝑅 ) ∧ Rel 𝑅 ) )
7		symrefref2	⊢ ( ◡ 𝑅 ⊆ 𝑅 → ( ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ 𝑅 ↔ ( I ↾ dom 𝑅 ) ⊆ 𝑅 ) )
8	7	pm5.32ri	⊢ ( ( ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ 𝑅 ∧ ◡ 𝑅 ⊆ 𝑅 ) ↔ ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ ◡ 𝑅 ⊆ 𝑅 ) )
9	8	anbi1i	⊢ ( ( ( ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ 𝑅 ∧ ◡ 𝑅 ⊆ 𝑅 ) ∧ Rel 𝑅 ) ↔ ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ ◡ 𝑅 ⊆ 𝑅 ) ∧ Rel 𝑅 ) )
10	6 9	bitri	⊢ ( ( RefRel 𝑅 ∧ SymRel 𝑅 ) ↔ ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ ◡ 𝑅 ⊆ 𝑅 ) ∧ Rel 𝑅 ) )