Metamath Proof Explorer

Theorem xpidtr

Description: A Cartesian square is a transitive relation. (Contributed by FL, 31-Jul-2009)

Ref Expression
Assertion xpidtr 
|- ( ( A X. A ) o. ( A X. A ) ) C_ ( A X. A )

Proof

Step Hyp Ref Expression
1 brxp 
 |-  ( x ( A X. A ) y <-> ( x e. A /\ y e. A ) )
2 brxp 
 |-  ( y ( A X. A ) z <-> ( y e. A /\ z e. A ) )
3 brxp 
 |-  ( x ( A X. A ) z <-> ( x e. A /\ z e. A ) )
4 3 simplbi2com 
 |-  ( z e. A -> ( x e. A -> x ( A X. A ) z ) )
5 2 4 simplbiim 
 |-  ( y ( A X. A ) z -> ( x e. A -> x ( A X. A ) z ) )
6 5 com12 
 |-  ( x e. A -> ( y ( A X. A ) z -> x ( A X. A ) z ) )
7 6 adantr 
 |-  ( ( x e. A /\ y e. A ) -> ( y ( A X. A ) z -> x ( A X. A ) z ) )
8 1 7 sylbi 
 |-  ( x ( A X. A ) y -> ( y ( A X. A ) z -> x ( A X. A ) z ) )
9 8 imp 
 |-  ( ( x ( A X. A ) y /\ y ( A X. A ) z ) -> x ( A X. A ) z )
10 9 ax-gen 
 |-  A. z ( ( x ( A X. A ) y /\ y ( A X. A ) z ) -> x ( A X. A ) z )
11 10 gen2 
 |-  A. x A. y A. z ( ( x ( A X. A ) y /\ y ( A X. A ) z ) -> x ( A X. A ) z )
12 cotr 
 |-  ( ( ( A X. A ) o. ( A X. A ) ) C_ ( A X. A ) <-> A. x A. y A. z ( ( x ( A X. A ) y /\ y ( A X. A ) z ) -> x ( A X. A ) z ) )
13 11 12 mpbir 
 |-  ( ( A X. A ) o. ( A X. A ) ) C_ ( A X. A )