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 | elrefsymrels3 | ⊢ ( 𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ( ( ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) ∧ 𝑅 ∈ Rels ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elrefsymrels2 | ⊢ ( 𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ ◡ 𝑅 ⊆ 𝑅 ) ∧ 𝑅 ∈ Rels ) ) | |
| 2 | idrefALT | ⊢ ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ↔ ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ) | |
| 3 | cnvsym | ⊢ ( ◡ 𝑅 ⊆ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) | |
| 4 | 2 3 | anbi12i | ⊢ ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ ◡ 𝑅 ⊆ 𝑅 ) ↔ ( ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) ) |
| 5 | 4 | anbi1i | ⊢ ( ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ ◡ 𝑅 ⊆ 𝑅 ) ∧ 𝑅 ∈ Rels ) ↔ ( ( ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) ∧ 𝑅 ∈ Rels ) ) |
| 6 | 1 5 | bitri | ⊢ ( 𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ( ( ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) ∧ 𝑅 ∈ Rels ) ) |