Theorem setscom 13121

Description: Different components can be set in any order. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)

Hypotheses

Ref	Expression
setscom.1	|- A e. _V
setscom.2	|- B e. _V

Assertion

Ref	Expression
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 of Theorem setscom

Step	Hyp	Ref	Expression
1		rescom 5038	. . . . . 6 |- ( ( S |` ( _V \ { A } ) ) |` ( _V \ { B } ) ) = ( ( S |` ( _V \ { B } ) ) |` ( _V \ { A } ) )
2	1	uneq1i 3357	. . . . 5 |- ( ( ( S |` ( _V \ { A } ) ) |` ( _V \ { B } ) ) u. { <. A , C >. } ) = ( ( ( S |` ( _V \ { B } ) ) |` ( _V \ { A } ) ) u. { <. A , C >. } )
3	2	uneq1i 3357	. . . 4 |- ( ( ( ( S |` ( _V \ { A } ) ) |` ( _V \ { B } ) ) u. { <. A , C >. } ) u. { <. B , D >. } ) = ( ( ( ( S |` ( _V \ { B } ) ) |` ( _V \ { A } ) ) u. { <. A , C >. } ) u. { <. B , D >. } )
4		un23 3366	. . . 4 |- ( ( ( ( S |` ( _V \ { B } ) ) |` ( _V \ { A } ) ) u. { <. A , C >. } ) u. { <. B , D >. } ) = ( ( ( ( S |` ( _V \ { B } ) ) |` ( _V \ { A } ) ) u. { <. B , D >. } ) u. { <. A , C >. } )
5	3, 4	eqtri 2252	. . 3 |- ( ( ( ( S |` ( _V \ { A } ) ) |` ( _V \ { B } ) ) u. { <. A , C >. } ) u. { <. B , D >. } ) = ( ( ( ( S |` ( _V \ { B } ) ) |` ( _V \ { A } ) ) u. { <. B , D >. } ) u. { <. A , C >. } )
6		setscom.1	. . . . . . . 8 |- A e. _V
7		setsvala 13112	. . . . . . . 8 |- ( ( S e. V /\ A e. _V /\ C e. W ) -> ( S sSet <. A , C >. ) = ( ( S |` ( _V \ { A } ) ) u. { <. A , C >. } ) )
8	6, 7	mp3an2 1361	. . . . . . 7 |- ( ( S e. V /\ C e. W ) -> ( S sSet <. A , C >. ) = ( ( S |` ( _V \ { A } ) ) u. { <. A , C >. } ) )
9	8	ad2ant2r 509	. . . . . 6 |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> ( S sSet <. A , C >. ) = ( ( S |` ( _V \ { A } ) ) u. { <. A , C >. } ) )
10	9	reseq1d 5012	. . . . 5 |- ( ( ( 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 5027	. . . . . 6 |- ( ( ( S |` ( _V \ { A } ) ) u. { <. A , C >. } ) |` ( _V \ { B } ) ) = ( ( ( S |` ( _V \ { A } ) ) |` ( _V \ { B } ) ) u. ( { <. A , C >. } |` ( _V \ { B } ) ) )
12		elex 2814	. . . . . . . . . . 11 |- ( C e. W -> C e. _V )
13	12	ad2antrl 490	. . . . . . . . . 10 |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> C e. _V )
14		opelxpi 4757	. . . . . . . . . 10 |- ( ( A e. _V /\ C e. _V ) -> <. A , C >. e. ( _V X. _V ) )
15	6, 13, 14	sylancr 414	. . . . . . . . 9 |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> <. A , C >. e. ( _V X. _V ) )
16		opexg 4320	. . . . . . . . . . 11 |- ( ( A e. _V /\ C e. _V ) -> <. A , C >. e. _V )
17	6, 13, 16	sylancr 414	. . . . . . . . . 10 |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> <. A , C >. e. _V )
18		relsng 4829	. . . . . . . . . 10 |- ( <. A , C >. e. _V -> ( Rel { <. A , C >. } <-> <. A , C >. e. ( _V X. _V ) ) )
19	17, 18	syl 14	. . . . . . . . 9 |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> ( Rel { <. A , C >. } <-> <. A , C >. e. ( _V X. _V ) ) )
20	15, 19	mpbird 167	. . . . . . . 8 |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> Rel { <. A , C >. } )
21		dmsnopg 5208	. . . . . . . . . 10 |- ( C e. _V -> dom { <. A , C >. } = { A } )
22	13, 21	syl 14	. . . . . . . . 9 |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> dom { <. A , C >. } = { A } )
23		disjsn2 3732	. . . . . . . . . . 11 |- ( A =/= B -> ( { A } i^i { B } ) = (/) )
24	23	ad2antlr 489	. . . . . . . . . 10 |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> ( { A } i^i { B } ) = (/) )
25		disj2 3550	. . . . . . . . . 10 |- ( ( { A } i^i { B } ) = (/) <-> { A } C_ ( _V \ { B } ) )
26	24, 25	sylib 122	. . . . . . . . 9 |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> { A } C_ ( _V \ { B } ) )
27	22, 26	eqsstrd 3263	. . . . . . . 8 |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> dom { <. A , C >. } C_ ( _V \ { B } ) )
28		relssres 5051	. . . . . . . 8 |- ( ( Rel { <. A , C >. } /\ dom { <. A , C >. } C_ ( _V \ { B } ) ) -> ( { <. A , C >. } |` ( _V \ { B } ) ) = { <. A , C >. } )
29	20, 27, 28	syl2anc 411	. . . . . . 7 |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> ( { <. A , C >. } |` ( _V \ { B } ) ) = { <. A , C >. } )
30	29	uneq2d 3361	. . . . . 6 |- ( ( ( 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 >. } ) )
31	11, 30	eqtrid 2276	. . . . 5 |- ( ( ( 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 >. } ) )
32	10, 31	eqtrd 2264	. . . 4 |- ( ( ( 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 >. } ) )
33	32	uneq1d 3360	. . 3 |- ( ( ( 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 >. } ) )
34		setscom.2	. . . . . . . 8 |- B e. _V
35		setsvala 13112	. . . . . . . 8 |- ( ( S e. V /\ B e. _V /\ D e. X ) -> ( S sSet <. B , D >. ) = ( ( S |` ( _V \ { B } ) ) u. { <. B , D >. } ) )
36	34, 35	mp3an2 1361	. . . . . . 7 |- ( ( S e. V /\ D e. X ) -> ( S sSet <. B , D >. ) = ( ( S |` ( _V \ { B } ) ) u. { <. B , D >. } ) )
37	36	reseq1d 5012	. . . . . 6 |- ( ( S e. V /\ D e. X ) -> ( ( S sSet <. B , D >. ) |` ( _V \ { A } ) ) = ( ( ( S |` ( _V \ { B } ) ) u. { <. B , D >. } ) |` ( _V \ { A } ) ) )
38	37	ad2ant2rl 511	. . . . 5 |- ( ( ( 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 } ) ) )
39		resundir 5027	. . . . . 6 |- ( ( ( S |` ( _V \ { B } ) ) u. { <. B , D >. } ) |` ( _V \ { A } ) ) = ( ( ( S |` ( _V \ { B } ) ) |` ( _V \ { A } ) ) u. ( { <. B , D >. } |` ( _V \ { A } ) ) )
40		elex 2814	. . . . . . . . . . 11 |- ( D e. X -> D e. _V )
41	40	ad2antll 491	. . . . . . . . . 10 |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> D e. _V )
42		opelxpi 4757	. . . . . . . . . 10 |- ( ( B e. _V /\ D e. _V ) -> <. B , D >. e. ( _V X. _V ) )
43	34, 41, 42	sylancr 414	. . . . . . . . 9 |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> <. B , D >. e. ( _V X. _V ) )
44		opexg 4320	. . . . . . . . . . 11 |- ( ( B e. _V /\ D e. _V ) -> <. B , D >. e. _V )
45	34, 41, 44	sylancr 414	. . . . . . . . . 10 |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> <. B , D >. e. _V )
46		relsng 4829	. . . . . . . . . 10 |- ( <. B , D >. e. _V -> ( Rel { <. B , D >. } <-> <. B , D >. e. ( _V X. _V ) ) )
47	45, 46	syl 14	. . . . . . . . 9 |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> ( Rel { <. B , D >. } <-> <. B , D >. e. ( _V X. _V ) ) )
48	43, 47	mpbird 167	. . . . . . . 8 |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> Rel { <. B , D >. } )
49		dmsnopg 5208	. . . . . . . . . 10 |- ( D e. _V -> dom { <. B , D >. } = { B } )
50	41, 49	syl 14	. . . . . . . . 9 |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> dom { <. B , D >. } = { B } )
51		ssv 3249	. . . . . . . . . . 11 |- { A } C_ _V
52		ssv 3249	. . . . . . . . . . 11 |- { B } C_ _V
53		ssconb 3340	. . . . . . . . . . 11 |- ( ( { A } C_ _V /\ { B } C_ _V ) -> ( { A } C_ ( _V \ { B } ) <-> { B } C_ ( _V \ { A } ) ) )
54	51, 52, 53	mp2an 426	. . . . . . . . . 10 |- ( { A } C_ ( _V \ { B } ) <-> { B } C_ ( _V \ { A } ) )
55	26, 54	sylib 122	. . . . . . . . 9 |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> { B } C_ ( _V \ { A } ) )
56	50, 55	eqsstrd 3263	. . . . . . . 8 |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> dom { <. B , D >. } C_ ( _V \ { A } ) )
57		relssres 5051	. . . . . . . 8 |- ( ( Rel { <. B , D >. } /\ dom { <. B , D >. } C_ ( _V \ { A } ) ) -> ( { <. B , D >. } |` ( _V \ { A } ) ) = { <. B , D >. } )
58	48, 56, 57	syl2anc 411	. . . . . . 7 |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> ( { <. B , D >. } |` ( _V \ { A } ) ) = { <. B , D >. } )
59	58	uneq2d 3361	. . . . . 6 |- ( ( ( 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 >. } ) )
60	39, 59	eqtrid 2276	. . . . 5 |- ( ( ( 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 >. } ) )
61	38, 60	eqtrd 2264	. . . 4 |- ( ( ( 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 >. } ) )
62	61	uneq1d 3360	. . 3 |- ( ( ( 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 >. } ) )
63	5, 33, 62	3eqtr4a 2290	. 2 |- ( ( ( 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 >. } ) )
64		setsex 13113	. . . . 5 |- ( ( S e. V /\ A e. _V /\ C e. W ) -> ( S sSet <. A , C >. ) e. _V )
65	6, 64	mp3an2 1361	. . . 4 |- ( ( S e. V /\ C e. W ) -> ( S sSet <. A , C >. ) e. _V )
66	65	ad2ant2r 509	. . 3 |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> ( S sSet <. A , C >. ) e. _V )
67	34	a1i 9	. . 3 |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> B e. _V )
68		simprr 533	. . 3 |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> D e. X )
69		setsvala 13112	. . 3 |- ( ( ( S sSet <. A , C >. ) e. _V /\ B e. _V /\ D e. X ) -> ( ( S sSet <. A , C >. ) sSet <. B , D >. ) = ( ( ( S sSet <. A , C >. ) |` ( _V \ { B } ) ) u. { <. B , D >. } ) )
70	66, 67, 68, 69	syl3anc 1273	. 2 |- ( ( ( 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 >. } ) )
71		setsex 13113	. . . . 5 |- ( ( S e. V /\ B e. _V /\ D e. X ) -> ( S sSet <. B , D >. ) e. _V )
72	34, 71	mp3an2 1361	. . . 4 |- ( ( S e. V /\ D e. X ) -> ( S sSet <. B , D >. ) e. _V )
73	72	ad2ant2rl 511	. . 3 |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> ( S sSet <. B , D >. ) e. _V )
74	6	a1i 9	. . 3 |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> A e. _V )
75		simprl 531	. . 3 |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> C e. W )
76		setsvala 13112	. . 3 |- ( ( ( S sSet <. B , D >. ) e. _V /\ A e. _V /\ C e. W ) -> ( ( S sSet <. B , D >. ) sSet <. A , C >. ) = ( ( ( S sSet <. B , D >. ) |` ( _V \ { A } ) ) u. { <. A , C >. } ) )
77	73, 74, 75, 76	syl3anc 1273	. 2 |- ( ( ( 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 >. } ) )
78	63, 70, 77	3eqtr4d 2274	1 |- ( ( ( 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 >. ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1397   e. wcel 2202   =/= wne 2402   _Vcvv 2802   \ cdif 3197   u. cun 3198   i^i cin 3199   C_ wss 3200   (/)c0 3494   {csn 3669   <.cop 3672   X. cxp 4723   dom cdm 4725   |` cres 4727   Rel wrel 4730  (class class class)co 6017   sSet csts 13079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299  ax-un 4530  ax-setind 4635

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-ral 2515  df-rex 2516  df-rab 2519  df-v 2804  df-sbc 3032  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-nul 3495  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-opab 4151  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-res 4737  df-iota 5286  df-fun 5328  df-fv 5334  df-ov 6020  df-oprab 6021  df-mpo 6022  df-sets 13088

This theorem is referenced by:  setscomd  13122