This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Power Sets Relations relcoi1
Description: Composition with the identity relation restricted to a relation's field.
(Contributed by FL , 8-May-2011) (Proof shortened by OpenAI , 3-Jul-2020)
Ref
Expression
Assertion
relcoi1 ⊢ ( Rel 𝑅 → ( 𝑅 ∘ ( I ↾ ∪ ∪ 𝑅 ) ) = 𝑅 )
Proof
Step
Hyp
Ref
Expression
1
coires1 ⊢ ( 𝑅 ∘ ( I ↾ ∪ ∪ 𝑅 ) ) = ( 𝑅 ↾ ∪ ∪ 𝑅 )
2
relresfld ⊢ ( Rel 𝑅 → ( 𝑅 ↾ ∪ ∪ 𝑅 ) = 𝑅 )
3
1 2
eqtrid ⊢ ( Rel 𝑅 → ( 𝑅 ∘ ( I ↾ ∪ ∪ 𝑅 ) ) = 𝑅 )