This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem inxpss2

Description: Two ways to say that intersections with Cartesian products are in a subclass relation. (Contributed by Peter Mazsa, 8-Mar-2019)

Ref Expression
Assertion inxpss2 
|- ( ( R i^i ( A X. B ) ) C_ ( S i^i ( A X. B ) ) <-> A. x e. A A. y e. B ( x R y -> x S y ) )

Proof

Step Hyp Ref Expression
1 relinxp 
 |-  Rel ( R i^i ( A X. B ) )
2 ssrel3 
 |-  ( Rel ( R i^i ( A X. B ) ) -> ( ( R i^i ( A X. B ) ) C_ ( S i^i ( A X. B ) ) <-> A. x A. y ( x ( R i^i ( A X. B ) ) y -> x ( S i^i ( A X. B ) ) y ) ) )
3 1 2 ax-mp 
 |-  ( ( R i^i ( A X. B ) ) C_ ( S i^i ( A X. B ) ) <-> A. x A. y ( x ( R i^i ( A X. B ) ) y -> x ( S i^i ( A X. B ) ) y ) )
4 inxpss3 
 |-  ( A. x A. y ( x ( R i^i ( A X. B ) ) y -> x ( S i^i ( A X. B ) ) y ) <-> A. x e. A A. y e. B ( x R y -> x S y ) )
5 3 4 bitri 
 |-  ( ( R i^i ( A X. B ) ) C_ ( S i^i ( A X. B ) ) <-> A. x e. A A. y e. B ( x R y -> x S y ) )