refsymrels3

Description: Elements of the class of reflexive relations which are elements of the class of symmetric relations as well (like the elements of the class of equivalence relations dfeqvrels3 ) can use the A. x e. dom r x r x version for their reflexive part, not just the A. x e. dom r A. y e. ran r ( x = y -> x r y ) version of dfrefrels3 , cf. the comment of dfrefrel3 . (Contributed by Peter Mazsa, 22-Jul-2019) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	refsymrels3	⊢ ( RefRels ∩ SymRels ) = { 𝑟 ∈ Rels ∣ ( ∀ 𝑥 ∈ dom 𝑟 𝑥 𝑟 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑟 𝑦 → 𝑦 𝑟 𝑥 ) ) }

Proof

Step	Hyp	Ref	Expression
1		refsymrels2	⊢ ( RefRels ∩ SymRels ) = { 𝑟 ∈ Rels ∣ ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ ^◡ 𝑟 ⊆ 𝑟 ) }
2		idrefALT	⊢ ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ↔ ∀ 𝑥 ∈ dom 𝑟 𝑥 𝑟 𝑥 )
3		cnvsym	⊢ ( ^◡ 𝑟 ⊆ 𝑟 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑟 𝑦 → 𝑦 𝑟 𝑥 ) )
4	2 3	anbi12i	⊢ ( ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ ^◡ 𝑟 ⊆ 𝑟 ) ↔ ( ∀ 𝑥 ∈ dom 𝑟 𝑥 𝑟 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑟 𝑦 → 𝑦 𝑟 𝑥 ) ) )
5	1 4	rabbieq	⊢ ( RefRels ∩ SymRels ) = { 𝑟 ∈ Rels ∣ ( ∀ 𝑥 ∈ dom 𝑟 𝑥 𝑟 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑟 𝑦 → 𝑦 𝑟 𝑥 ) ) }

Metamath Proof Explorer

Theorem refsymrels3

Proof