Theorem refsymrels2 39023

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 39046) can use the restricted version for their reflexive part (see below), not just the ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟 version of dfrefrels2 38967, cf. the comment of dfrefrels2 38967. (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 38967	. . 3 ⊢ RefRels = {𝑟 ∈ Rels ∣ ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟}
2		dfsymrels2 38999	. . 3 ⊢ SymRels = {𝑟 ∈ Rels ∣ ◡𝑟 ⊆ 𝑟}
3	1, 2	ineq12i 4154	. 2 ⊢ ( RefRels ∩ SymRels ) = ({𝑟 ∈ Rels ∣ ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟} ∩ {𝑟 ∈ Rels ∣ ◡𝑟 ⊆ 𝑟})
4		inrab 4251	. 2 ⊢ ({𝑟 ∈ Rels ∣ ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟} ∩ {𝑟 ∈ Rels ∣ ◡𝑟 ⊆ 𝑟}) = {𝑟 ∈ Rels ∣ (( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟)}
5		symrefref2 39021	. . . 4 ⊢ (◡𝑟 ⊆ 𝑟 → (( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟 ↔ ( I ↾ dom 𝑟) ⊆ 𝑟))
6	5	pm5.32ri 580	. . 3 ⊢ ((( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟) ↔ (( I ↾ dom 𝑟) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟))
7	6	rabbii 3397	. 2 ⊢ {𝑟 ∈ Rels ∣ (( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟)} = {𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟)}
8	3, 4, 7	3eqtri 2767	1 ⊢ ( RefRels ∩ SymRels ) = {𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟)}

Syntax hints:   ∧ wa 396   = wceq 1547  {crab 3392   ∩ cin 3889   ⊆ wss 3890   I cid 5519   × cxp 5623  ^◡ccnv 5624  dom cdm 5625  ran crn 5626   ↾ cres 5627   Rels crels 38559   RefRels crefrels 38562   SymRels csymrels 38568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-dm 5635  df-rn 5636  df-res 5637  df-rels 38814  df-ssr 38952  df-refs 38964  df-refrels 38965  df-syms 38996  df-symrels 38997

This theorem is referenced by:  refsymrels3  39024  elrefsymrels2  39027  dfeqvrels2  39046  refrelsredund4  39090