Metamath Proof Explorer

Theorem setscom

Description: Component-setting is commutative when the x-values are different. (Contributed by Mario Carneiro, 5-Dec-2014) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Hypotheses setscom.1 
|- A e. _V
setscom.2 
|- B e. _V
Assertion setscom 
|- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> ( ( S sSet <. A , C >. ) sSet <. B , D >. ) = ( ( S sSet <. B , D >. ) sSet <. A , C >. ) )

Proof

Step Hyp Ref Expression
1 setscom.1 
 |-  A e. _V
2 setscom.2 
 |-  B e. _V
3 rescom 
 |-  ( ( S |` ( _V \ { A } ) ) |` ( _V \ { B } ) ) = ( ( S |` ( _V \ { B } ) ) |` ( _V \ { A } ) )
4 3 uneq1i 
 |-  ( ( ( S |` ( _V \ { A } ) ) |` ( _V \ { B } ) ) u. { <. A , C >. } ) = ( ( ( S |` ( _V \ { B } ) ) |` ( _V \ { A } ) ) u. { <. A , C >. } )
5 4 uneq1i 
 |-  ( ( ( ( S |` ( _V \ { A } ) ) |` ( _V \ { B } ) ) u. { <. A , C >. } ) u. { <. B , D >. } ) = ( ( ( ( S |` ( _V \ { B } ) ) |` ( _V \ { A } ) ) u. { <. A , C >. } ) u. { <. B , D >. } )
6 un23 
 |-  ( ( ( ( S |` ( _V \ { B } ) ) |` ( _V \ { A } ) ) u. { <. A , C >. } ) u. { <. B , D >. } ) = ( ( ( ( S |` ( _V \ { B } ) ) |` ( _V \ { A } ) ) u. { <. B , D >. } ) u. { <. A , C >. } )
7 5 6 eqtri 
 |-  ( ( ( ( S |` ( _V \ { A } ) ) |` ( _V \ { B } ) ) u. { <. A , C >. } ) u. { <. B , D >. } ) = ( ( ( ( S |` ( _V \ { B } ) ) |` ( _V \ { A } ) ) u. { <. B , D >. } ) u. { <. A , C >. } )
8 setsval 
 |-  ( ( S e. V /\ C e. W ) -> ( S sSet <. A , C >. ) = ( ( S |` ( _V \ { A } ) ) u. { <. A , C >. } ) )
9 8 ad2ant2r 
 |-  ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> ( S sSet <. A , C >. ) = ( ( S |` ( _V \ { A } ) ) u. { <. A , C >. } ) )
10 9 reseq1d 
 |-  ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> ( ( S sSet <. A , C >. ) |` ( _V \ { B } ) ) = ( ( ( S |` ( _V \ { A } ) ) u. { <. A , C >. } ) |` ( _V \ { B } ) ) )
11 resundir 
 |-  ( ( ( S |` ( _V \ { A } ) ) u. { <. A , C >. } ) |` ( _V \ { B } ) ) = ( ( ( S |` ( _V \ { A } ) ) |` ( _V \ { B } ) ) u. ( { <. A , C >. } |` ( _V \ { B } ) ) )
12 elex 
 |-  ( C e. W -> C e. _V )
13 12 ad2antrl 
 |-  ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> C e. _V )
14 opelxpi 
 |-  ( ( A e. _V /\ C e. _V ) -> <. A , C >. e. ( _V X. _V ) )
15 1 13 14 sylancr 
 |-  ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> <. A , C >. e. ( _V X. _V ) )
16 opex 
 |-  <. A , C >. e. _V
17 16 relsn 
 |-  ( Rel { <. A , C >. } <-> <. A , C >. e. ( _V X. _V ) )
18 15 17 sylibr 
 |-  ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> Rel { <. A , C >. } )
19 dmsnopss 
 |-  dom { <. A , C >. } C_ { A }
20 disjsn2 
 |-  ( A =/= B -> ( { A } i^i { B } ) = (/) )
21 20 ad2antlr 
 |-  ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> ( { A } i^i { B } ) = (/) )
22 disj2 
 |-  ( ( { A } i^i { B } ) = (/) <-> { A } C_ ( _V \ { B } ) )
23 21 22 sylib 
 |-  ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> { A } C_ ( _V \ { B } ) )
24 19 23 sstrid 
 |-  ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> dom { <. A , C >. } C_ ( _V \ { B } ) )
25 relssres 
 |-  ( ( Rel { <. A , C >. } /\ dom { <. A , C >. } C_ ( _V \ { B } ) ) -> ( { <. A , C >. } |` ( _V \ { B } ) ) = { <. A , C >. } )
26 18 24 25 syl2anc 
 |-  ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> ( { <. A , C >. } |` ( _V \ { B } ) ) = { <. A , C >. } )
27 26 uneq2d 
 |-  ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> ( ( ( S |` ( _V \ { A } ) ) |` ( _V \ { B } ) ) u. ( { <. A , C >. } |` ( _V \ { B } ) ) ) = ( ( ( S |` ( _V \ { A } ) ) |` ( _V \ { B } ) ) u. { <. A , C >. } ) )
28 11 27 syl5eq 
 |-  ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> ( ( ( S |` ( _V \ { A } ) ) u. { <. A , C >. } ) |` ( _V \ { B } ) ) = ( ( ( S |` ( _V \ { A } ) ) |` ( _V \ { B } ) ) u. { <. A , C >. } ) )
29 10 28 eqtrd 
 |-  ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> ( ( S sSet <. A , C >. ) |` ( _V \ { B } ) ) = ( ( ( S |` ( _V \ { A } ) ) |` ( _V \ { B } ) ) u. { <. A , C >. } ) )
30 29 uneq1d 
 |-  ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> ( ( ( S sSet <. A , C >. ) |` ( _V \ { B } ) ) u. { <. B , D >. } ) = ( ( ( ( S |` ( _V \ { A } ) ) |` ( _V \ { B } ) ) u. { <. A , C >. } ) u. { <. B , D >. } ) )
31 setsval 
 |-  ( ( S e. V /\ D e. X ) -> ( S sSet <. B , D >. ) = ( ( S |` ( _V \ { B } ) ) u. { <. B , D >. } ) )
32 31 reseq1d 
 |-  ( ( S e. V /\ D e. X ) -> ( ( S sSet <. B , D >. ) |` ( _V \ { A } ) ) = ( ( ( S |` ( _V \ { B } ) ) u. { <. B , D >. } ) |` ( _V \ { A } ) ) )
33 32 ad2ant2rl 
 |-  ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> ( ( S sSet <. B , D >. ) |` ( _V \ { A } ) ) = ( ( ( S |` ( _V \ { B } ) ) u. { <. B , D >. } ) |` ( _V \ { A } ) ) )
34 resundir 
 |-  ( ( ( S |` ( _V \ { B } ) ) u. { <. B , D >. } ) |` ( _V \ { A } ) ) = ( ( ( S |` ( _V \ { B } ) ) |` ( _V \ { A } ) ) u. ( { <. B , D >. } |` ( _V \ { A } ) ) )
35 elex 
 |-  ( D e. X -> D e. _V )
36 35 ad2antll 
 |-  ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> D e. _V )
37 opelxpi 
 |-  ( ( B e. _V /\ D e. _V ) -> <. B , D >. e. ( _V X. _V ) )
38 2 36 37 sylancr 
 |-  ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> <. B , D >. e. ( _V X. _V ) )
39 opex 
 |-  <. B , D >. e. _V
40 39 relsn 
 |-  ( Rel { <. B , D >. } <-> <. B , D >. e. ( _V X. _V ) )
41 38 40 sylibr 
 |-  ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> Rel { <. B , D >. } )
42 dmsnopss 
 |-  dom { <. B , D >. } C_ { B }
43 ssv 
 |-  { A } C_ _V
44 ssv 
 |-  { B } C_ _V
45 ssconb 
 |-  ( ( { A } C_ _V /\ { B } C_ _V ) -> ( { A } C_ ( _V \ { B } ) <-> { B } C_ ( _V \ { A } ) ) )
46 43 44 45 mp2an 
 |-  ( { A } C_ ( _V \ { B } ) <-> { B } C_ ( _V \ { A } ) )
47 23 46 sylib 
 |-  ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> { B } C_ ( _V \ { A } ) )
48 42 47 sstrid 
 |-  ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> dom { <. B , D >. } C_ ( _V \ { A } ) )
49 relssres 
 |-  ( ( Rel { <. B , D >. } /\ dom { <. B , D >. } C_ ( _V \ { A } ) ) -> ( { <. B , D >. } |` ( _V \ { A } ) ) = { <. B , D >. } )
50 41 48 49 syl2anc 
 |-  ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> ( { <. B , D >. } |` ( _V \ { A } ) ) = { <. B , D >. } )
51 50 uneq2d 
 |-  ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> ( ( ( S |` ( _V \ { B } ) ) |` ( _V \ { A } ) ) u. ( { <. B , D >. } |` ( _V \ { A } ) ) ) = ( ( ( S |` ( _V \ { B } ) ) |` ( _V \ { A } ) ) u. { <. B , D >. } ) )
52 34 51 syl5eq 
 |-  ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> ( ( ( S |` ( _V \ { B } ) ) u. { <. B , D >. } ) |` ( _V \ { A } ) ) = ( ( ( S |` ( _V \ { B } ) ) |` ( _V \ { A } ) ) u. { <. B , D >. } ) )
53 33 52 eqtrd 
 |-  ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> ( ( S sSet <. B , D >. ) |` ( _V \ { A } ) ) = ( ( ( S |` ( _V \ { B } ) ) |` ( _V \ { A } ) ) u. { <. B , D >. } ) )
54 53 uneq1d 
 |-  ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> ( ( ( S sSet <. B , D >. ) |` ( _V \ { A } ) ) u. { <. A , C >. } ) = ( ( ( ( S |` ( _V \ { B } ) ) |` ( _V \ { A } ) ) u. { <. B , D >. } ) u. { <. A , C >. } ) )
55 7 30 54 3eqtr4a 
 |-  ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> ( ( ( S sSet <. A , C >. ) |` ( _V \ { B } ) ) u. { <. B , D >. } ) = ( ( ( S sSet <. B , D >. ) |` ( _V \ { A } ) ) u. { <. A , C >. } ) )
56 ovex 
 |-  ( S sSet <. A , C >. ) e. _V
57 simprr 
 |-  ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> D e. X )
58 setsval 
 |-  ( ( ( S sSet <. A , C >. ) e. _V /\ D e. X ) -> ( ( S sSet <. A , C >. ) sSet <. B , D >. ) = ( ( ( S sSet <. A , C >. ) |` ( _V \ { B } ) ) u. { <. B , D >. } ) )
59 56 57 58 sylancr 
 |-  ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> ( ( S sSet <. A , C >. ) sSet <. B , D >. ) = ( ( ( S sSet <. A , C >. ) |` ( _V \ { B } ) ) u. { <. B , D >. } ) )
60 ovex 
 |-  ( S sSet <. B , D >. ) e. _V
61 simprl 
 |-  ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> C e. W )
62 setsval 
 |-  ( ( ( S sSet <. B , D >. ) e. _V /\ C e. W ) -> ( ( S sSet <. B , D >. ) sSet <. A , C >. ) = ( ( ( S sSet <. B , D >. ) |` ( _V \ { A } ) ) u. { <. A , C >. } ) )
63 60 61 62 sylancr 
 |-  ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> ( ( S sSet <. B , D >. ) sSet <. A , C >. ) = ( ( ( S sSet <. B , D >. ) |` ( _V \ { A } ) ) u. { <. A , C >. } ) )
64 55 59 63 3eqtr4d 
 |-  ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> ( ( S sSet <. A , C >. ) sSet <. B , D >. ) = ( ( S sSet <. B , D >. ) sSet <. A , C >. ) )