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 relres
Description: A restriction is a relation. Exercise 12 of TakeutiZaring p. 25.
(Contributed by NM , 2-Aug-1994) (Proof shortened by Andrew Salmon , 27-Aug-2011)
Ref
Expression
Assertion
relres ⊢ Rel ( 𝐴 ↾ 𝐵 )
Proof
Step
Hyp
Ref
Expression
1
df-res ⊢ ( 𝐴 ↾ 𝐵 ) = ( 𝐴 ∩ ( 𝐵 × V ) )
2
inss2 ⊢ ( 𝐴 ∩ ( 𝐵 × V ) ) ⊆ ( 𝐵 × V )
3
1 2
eqsstri ⊢ ( 𝐴 ↾ 𝐵 ) ⊆ ( 𝐵 × V )
4
relxp ⊢ Rel ( 𝐵 × V )
5
relss ⊢ ( ( 𝐴 ↾ 𝐵 ) ⊆ ( 𝐵 × V ) → ( Rel ( 𝐵 × V ) → Rel ( 𝐴 ↾ 𝐵 ) ) )
6
3 4 5
mp2 ⊢ Rel ( 𝐴 ↾ 𝐵 )