Theorem dfrefrel3 39720

Description: Alternate definition of the reflexive relation predicate. A relation is reflexive iff: for all elements on its domain and range, if an element of its domain is the same as an element of its range, then there is the relation between them.

Note that this is definitely not the definition we are accustomed to, like e.g. idref 7173 / idrefALT 6119 or df-reflexive 51144 ⊢ (𝑅 Reflexive 𝐴 ↔ (𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥 ∈ 𝐴𝑥𝑅𝑥)). It turns out that the not-surprising definition which contains ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥 needs symmetry as well, see refsymrels3 39774. Only when this symmetry condition holds, like in case of equivalence relations, see dfeqvrels3 39797, can we write the traditional form ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥 for reflexive relations. For the special case with square Cartesian product when the two forms are equivalent see idinxpssinxp4 39450 where ⊢ (∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 = 𝑦 → 𝑥𝑅𝑦) ↔ ∀𝑥 ∈ 𝐴𝑥𝑅𝑥). See also similar definition of the converse reflexive relations class dfcnvrefrel3 39735. (Contributed by Peter Mazsa, 8-Jul-2019.)

Assertion

Ref	Expression
dfrefrel3	⊢ ( RefRel 𝑅 ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) ∧ Rel 𝑅))

Distinct variable group:   𝑥,𝑅,𝑦

Proof of Theorem dfrefrel3

Step	Hyp	Ref	Expression
1		dfrefrel2 39719	. 2 ⊢ ( RefRel 𝑅 ↔ (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 ∧ Rel 𝑅))
2		idinxpss 39442	. . 3 ⊢ (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 ↔ ∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦))
3	2	anbi1i 636	. 2 ⊢ ((( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 ∧ Rel 𝑅) ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) ∧ Rel 𝑅))
4	1, 3	bitri 278	1 ⊢ ( RefRel 𝑅 ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) ∧ Rel 𝑅))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wral 3080   ⊆ wss 3900   ∩ cin 4092   class class class wbr 5106   I cid 5549   × cxp 5653  dom cdm 5655  ran crn 5656  Rel wrel 5660   RefRel wrefrel 39313

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-dm 5665  df-rn 5666  df-res 5667  df-refrel 39716

This theorem is used by:  refsymrel3  39776