Theorem refsymrels2 38818

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 dfeqvrels2 38841) can use the restricted version for their reflexive part (see below), not just the ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟 version of dfrefrels2 38762, cf. the comment of dfrefrels2 38762. (Contributed by Peter Mazsa, 20-Jul-2019.)

Assertion

Ref	Expression
refsymrels2	⊢ ( RefRels ∩ SymRels ) = {𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟)}

Proof of Theorem refsymrels2

Step	Hyp	Ref	Expression
1		dfrefrels2 38762	. . 3 ⊢ RefRels = {𝑟 ∈ Rels ∣ ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟}
2		dfsymrels2 38794	. . 3 ⊢ SymRels = {𝑟 ∈ Rels ∣ ◡𝑟 ⊆ 𝑟}
3	1, 2	ineq12i 4170	. 2 ⊢ ( RefRels ∩ SymRels ) = ({𝑟 ∈ Rels ∣ ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟} ∩ {𝑟 ∈ Rels ∣ ◡𝑟 ⊆ 𝑟})
4		inrab 4268	. 2 ⊢ ({𝑟 ∈ Rels ∣ ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟} ∩ {𝑟 ∈ Rels ∣ ◡𝑟 ⊆ 𝑟}) = {𝑟 ∈ Rels ∣ (( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟)}
5		symrefref2 38816	. . . 4 ⊢ (◡𝑟 ⊆ 𝑟 → (( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟 ↔ ( I ↾ dom 𝑟) ⊆ 𝑟))
6	5	pm5.32ri 575	. . 3 ⊢ ((( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟) ↔ (( I ↾ dom 𝑟) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟))
7	6	rabbii 3404	. 2 ⊢ {𝑟 ∈ Rels ∣ (( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟)} = {𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟)}
8	3, 4, 7	3eqtri 2763	1 ⊢ ( RefRels ∩ SymRels ) = {𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟)}

Syntax hints:   ∧ wa 395   = wceq 1541  {crab 3399   ∩ cin 3900   ⊆ wss 3901   I cid 5518   × cxp 5622  ^◡ccnv 5623  dom cdm 5624  ran crn 5625   ↾ cres 5626   Rels crels 38381   RefRels crefrels 38384   SymRels csymrels 38390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-dm 5634  df-rn 5635  df-res 5636  df-rels 38621  df-ssr 38747  df-refs 38759  df-refrels 38760  df-syms 38791  df-symrels 38792

This theorem is referenced by:  refsymrels3  38819  elrefsymrels2  38822  dfeqvrels2  38841  refrelsredund4  38885