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 rnxpss
Description: The range of a Cartesian product is included in its second factor.
(Contributed by NM , 16-Jan-2006) (Proof shortened by Andrew Salmon , 27-Aug-2011)
Ref
Expression
Assertion
rnxpss ⊢ ran ( 𝐴 × 𝐵 ) ⊆ 𝐵
Proof
Step
Hyp
Ref
Expression
1
df-rn ⊢ ran ( 𝐴 × 𝐵 ) = dom ◡ 𝐴 × 𝐵 )
2
cnvxp ⊢ ◡ 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 )
3
2
dmeqi ⊢ dom ◡ 𝐴 × 𝐵 ) = dom ( 𝐵 × 𝐴 )
4
dmxpss ⊢ dom ( 𝐵 × 𝐴 ) ⊆ 𝐵
5
3 4
eqsstri ⊢ dom ◡ 𝐴 × 𝐵 ) ⊆ 𝐵
6
1 5
eqsstri ⊢ ran ( 𝐴 × 𝐵 ) ⊆ 𝐵