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

Metamath Proof Explorer

Theorem xptrrel

Description: The cross product is always a transitive relation. (Contributed by RP, 24-Dec-2019)

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

Proof

Step Hyp Ref Expression
1 inss1 
 |-  ( dom ( A X. B ) i^i ran ( A X. B ) ) C_ dom ( A X. B )
2 dmxpss 
 |-  dom ( A X. B ) C_ A
3 1 2 sstri 
 |-  ( dom ( A X. B ) i^i ran ( A X. B ) ) C_ A
4 inss2 
 |-  ( dom ( A X. B ) i^i ran ( A X. B ) ) C_ ran ( A X. B )
5 rnxpss 
 |-  ran ( A X. B ) C_ B
6 4 5 sstri 
 |-  ( dom ( A X. B ) i^i ran ( A X. B ) ) C_ B
7 3 6 ssini 
 |-  ( dom ( A X. B ) i^i ran ( A X. B ) ) C_ ( A i^i B )
8 eqimss 
 |-  ( ( A i^i B ) = (/) -> ( A i^i B ) C_ (/) )
9 7 8 sstrid 
 |-  ( ( A i^i B ) = (/) -> ( dom ( A X. B ) i^i ran ( A X. B ) ) C_ (/) )
10 ss0 
 |-  ( ( dom ( A X. B ) i^i ran ( A X. B ) ) C_ (/) -> ( dom ( A X. B ) i^i ran ( A X. B ) ) = (/) )
11 9 10 syl 
 |-  ( ( A i^i B ) = (/) -> ( dom ( A X. B ) i^i ran ( A X. B ) ) = (/) )
12 11 coemptyd 
 |-  ( ( A i^i B ) = (/) -> ( ( A X. B ) o. ( A X. B ) ) = (/) )
13 0ss 
 |-  (/) C_ ( A X. B )
14 12 13 eqsstrdi 
 |-  ( ( A i^i B ) = (/) -> ( ( A X. B ) o. ( A X. B ) ) C_ ( A X. B ) )
15 neqne 
 |-  ( -. ( A i^i B ) = (/) -> ( A i^i B ) =/= (/) )
16 15 xpcoidgend 
 |-  ( -. ( A i^i B ) = (/) -> ( ( A X. B ) o. ( A X. B ) ) = ( A X. B ) )
17 ssid 
 |-  ( A X. B ) C_ ( A X. B )
18 16 17 eqsstrdi 
 |-  ( -. ( A i^i B ) = (/) -> ( ( A X. B ) o. ( A X. B ) ) C_ ( A X. B ) )
19 14 18 pm2.61i 
 |-  ( ( A X. B ) o. ( A X. B ) ) C_ ( A X. B )