Metamath Proof Explorer

Theorem xpider

Description: A Cartesian square is an equivalence relation (in general, it is not a poset). (Contributed by FL, 31-Jul-2009) (Revised by Mario Carneiro, 12-Aug-2015)

Ref Expression
Assertion xpider 
|- ( A X. A ) Er A

Proof

Step Hyp Ref Expression
1 relxp 
 |-  Rel ( A X. A )
2 dmxpid 
 |-  dom ( A X. A ) = A
3 cnvxp 
 |-  `' ( A X. A ) = ( A X. A )
4 xpidtr 
 |-  ( ( A X. A ) o. ( A X. A ) ) C_ ( A X. A )
5 uneq1 
 |-  ( `' ( A X. A ) = ( A X. A ) -> ( `' ( A X. A ) u. ( A X. A ) ) = ( ( A X. A ) u. ( A X. A ) ) )
6 unss2 
 |-  ( ( ( A X. A ) o. ( A X. A ) ) C_ ( A X. A ) -> ( `' ( A X. A ) u. ( ( A X. A ) o. ( A X. A ) ) ) C_ ( `' ( A X. A ) u. ( A X. A ) ) )
7 unidm 
 |-  ( ( A X. A ) u. ( A X. A ) ) = ( A X. A )
8 eqtr 
 |-  ( ( ( `' ( A X. A ) u. ( A X. A ) ) = ( ( A X. A ) u. ( A X. A ) ) /\ ( ( A X. A ) u. ( A X. A ) ) = ( A X. A ) ) -> ( `' ( A X. A ) u. ( A X. A ) ) = ( A X. A ) )
9 sseq2 
 |-  ( ( `' ( A X. A ) u. ( A X. A ) ) = ( A X. A ) -> ( ( `' ( A X. A ) u. ( ( A X. A ) o. ( A X. A ) ) ) C_ ( `' ( A X. A ) u. ( A X. A ) ) <-> ( `' ( A X. A ) u. ( ( A X. A ) o. ( A X. A ) ) ) C_ ( A X. A ) ) )
10 9 biimpd 
 |-  ( ( `' ( A X. A ) u. ( A X. A ) ) = ( A X. A ) -> ( ( `' ( A X. A ) u. ( ( A X. A ) o. ( A X. A ) ) ) C_ ( `' ( A X. A ) u. ( A X. A ) ) -> ( `' ( A X. A ) u. ( ( A X. A ) o. ( A X. A ) ) ) C_ ( A X. A ) ) )
11 8 10 syl 
 |-  ( ( ( `' ( A X. A ) u. ( A X. A ) ) = ( ( A X. A ) u. ( A X. A ) ) /\ ( ( A X. A ) u. ( A X. A ) ) = ( A X. A ) ) -> ( ( `' ( A X. A ) u. ( ( A X. A ) o. ( A X. A ) ) ) C_ ( `' ( A X. A ) u. ( A X. A ) ) -> ( `' ( A X. A ) u. ( ( A X. A ) o. ( A X. A ) ) ) C_ ( A X. A ) ) )
12 7 11 mpan2 
 |-  ( ( `' ( A X. A ) u. ( A X. A ) ) = ( ( A X. A ) u. ( A X. A ) ) -> ( ( `' ( A X. A ) u. ( ( A X. A ) o. ( A X. A ) ) ) C_ ( `' ( A X. A ) u. ( A X. A ) ) -> ( `' ( A X. A ) u. ( ( A X. A ) o. ( A X. A ) ) ) C_ ( A X. A ) ) )
13 5 6 12 syl2im 
 |-  ( `' ( A X. A ) = ( A X. A ) -> ( ( ( A X. A ) o. ( A X. A ) ) C_ ( A X. A ) -> ( `' ( A X. A ) u. ( ( A X. A ) o. ( A X. A ) ) ) C_ ( A X. A ) ) )
14 3 4 13 mp2 
 |-  ( `' ( A X. A ) u. ( ( A X. A ) o. ( A X. A ) ) ) C_ ( A X. A )
15 df-er 
 |-  ( ( A X. A ) Er A <-> ( Rel ( A X. A ) /\ dom ( A X. A ) = A /\ ( `' ( A X. A ) u. ( ( A X. A ) o. ( A X. A ) ) ) C_ ( A X. A ) ) )
16 1 2 14 15 mpbir3an 
 |-  ( A X. A ) Er A