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

Metamath Proof Explorer

Theorem refsymrel3

Description: A relation which is reflexive and symmetric (like an equivalence relation) can use the A. x e. dom R x R x version for its reflexive part, not just the A. x e. dom R A. y e. ran R ( x = y -> x R y ) version of dfrefrel3 , cf. the comment of dfrefrel3 . (Contributed by Peter Mazsa, 23-Aug-2021)

Ref Expression
Assertion refsymrel3 ( ( RefRel 𝑅 ∧ SymRel 𝑅 ) ↔ ( ( ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) ∧ Rel 𝑅 ) )

Proof

Step Hyp Ref Expression
1 dfrefrel3 ⊢ ( RefRel 𝑅 ↔ ( ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) ∧ Rel 𝑅 ) )
2 dfsymrel3 ⊢ ( SymRel 𝑅 ↔ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ∧ Rel 𝑅 ) )
3 1 2 anbi12i ⊢ ( ( RefRel 𝑅 ∧ SymRel 𝑅 ) ↔ ( ( ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) ∧ Rel 𝑅 ) ∧ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ∧ Rel 𝑅 ) ) )
4 anandi3r ⊢ ( ( ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) ∧ Rel 𝑅 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) ↔ ( ( ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) ∧ Rel 𝑅 ) ∧ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ∧ Rel 𝑅 ) ) )
5 3anan32 ⊢ ( ( ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) ∧ Rel 𝑅 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) ↔ ( ( ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) ∧ Rel 𝑅 ) )
6 3 4 5 3bitr2i ⊢ ( ( RefRel 𝑅 ∧ SymRel 𝑅 ) ↔ ( ( ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) ∧ Rel 𝑅 ) )
7 symrefref3 ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) → ( ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) ↔ ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ) )
8 7 pm5.32ri ⊢ ( ( ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) ↔ ( ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) )
9 8 anbi1i ⊢ ( ( ( ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) ∧ Rel 𝑅 ) ↔ ( ( ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) ∧ Rel 𝑅 ) )
10 6 9 bitri ⊢ ( ( RefRel 𝑅 ∧ SymRel 𝑅 ) ↔ ( ( ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) ∧ Rel 𝑅 ) )