This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem symrefref3

Description: Symmetry is a sufficient condition for the equivalence of two versions of the reflexive relation, see also symrefref2 . (Contributed by Peter Mazsa, 23-Aug-2021) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	symrefref3	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) → ( ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) ↔ ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		symrefref2	⊢ ( ^◡ 𝑅 ⊆ 𝑅 → ( ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ 𝑅 ↔ ( I ↾ dom 𝑅 ) ⊆ 𝑅 ) )
2		cnvsym	⊢ ( ^◡ 𝑅 ⊆ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) )
3		idinxpss	⊢ ( ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ 𝑅 ↔ ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) )
4		idrefALT	⊢ ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ↔ ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 )
5	3 4	bibi12i	⊢ ( ( ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ 𝑅 ↔ ( I ↾ dom 𝑅 ) ⊆ 𝑅 ) ↔ ( ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) ↔ ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ) )
6	1 2 5	3imtr3i	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) → ( ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) ↔ ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ) )