Theorem refsymrels2 35816

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 35838) can use the restricted version for their reflexive part (see below), not just the ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟 version of dfrefrels2 35768, cf. the comment of dfrefrels2 35768. (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 35768	. . 3 ⊢ RefRels = {𝑟 ∈ Rels ∣ ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟}
2		dfsymrels2 35796	. . 3 ⊢ SymRels = {𝑟 ∈ Rels ∣ ◡𝑟 ⊆ 𝑟}
3	1, 2	ineq12i 4187	. 2 ⊢ ( RefRels ∩ SymRels ) = ({𝑟 ∈ Rels ∣ ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟} ∩ {𝑟 ∈ Rels ∣ ◡𝑟 ⊆ 𝑟})
4		inrab 4275	. 2 ⊢ ({𝑟 ∈ Rels ∣ ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟} ∩ {𝑟 ∈ Rels ∣ ◡𝑟 ⊆ 𝑟}) = {𝑟 ∈ Rels ∣ (( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟)}
5		symrefref2 35814	. . . 4 ⊢ (◡𝑟 ⊆ 𝑟 → (( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟 ↔ ( I ↾ dom 𝑟) ⊆ 𝑟))
6	5	pm5.32ri 578	. . 3 ⊢ ((( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟) ↔ (( I ↾ dom 𝑟) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟))
7	6	rabbii 3473	. 2 ⊢ {𝑟 ∈ Rels ∣ (( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟)} = {𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟)}
8	3, 4, 7	3eqtri 2848	1 ⊢ ( RefRels ∩ SymRels ) = {𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟)}

Syntax hints:   ∧ wa 398   = wceq 1537  {crab 3142   ∩ cin 3935   ⊆ wss 3936   I cid 5459   × cxp 5553  ^◡ccnv 5554  dom cdm 5555  ran crn 5556   ↾ cres 5557   Rels crels 35470   RefRels crefrels 35473   SymRels csymrels 35479

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-dm 5565  df-rn 5566  df-res 5567  df-rels 35740  df-ssr 35753  df-refs 35765  df-refrels 35766  df-syms 35793  df-symrels 35794

This theorem is referenced by:  refsymrels3  35817  elrefsymrels2  35820  dfeqvrels2  35838  refrelsredund4  35882