Theorem setscom 12872

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 4984	. . . . . 6 |- ( ( S |` ( _V \ { A } ) ) |` ( _V \ { B } ) ) = ( ( S |` ( _V \ { B } ) ) |` ( _V \ { A } ) )
2	1	uneq1i 3323	. . . . 5 |- ( ( ( S |` ( _V \ { A } ) ) |` ( _V \ { B } ) ) u. { <. A , C >. } ) = ( ( ( S |` ( _V \ { B } ) ) |` ( _V \ { A } ) ) u. { <. A , C >. } )
3	2	uneq1i 3323	. . . 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 3332	. . . 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 2226	. . 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 12863	. . . . . . . 8 |- ( ( S e. V /\ A e. _V /\ C e. W ) -> ( S sSet <. A , C >. ) = ( ( S |` ( _V \ { A } ) ) u. { <. A , C >. } ) )
8	6, 7	mp3an2 1338	. . . . . . 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 4958	. . . . 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 4973	. . . . . 6 |- ( ( ( S |` ( _V \ { A } ) ) u. { <. A , C >. } ) |` ( _V \ { B } ) ) = ( ( ( S |` ( _V \ { A } ) ) |` ( _V \ { B } ) ) u. ( { <. A , C >. } |` ( _V \ { B } ) ) )
12		elex 2783	. . . . . . . . . . 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 4707	. . . . . . . . . 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 4272	. . . . . . . . . . 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 4778	. . . . . . . . . 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 5154	. . . . . . . . . 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 3696	. . . . . . . . . . 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 3516	. . . . . . . . . 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 3229	. . . . . . . 8 |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> dom { <. A , C >. } C_ ( _V \ { B } ) )
28		relssres 4997	. . . . . . . 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 3327	. . . . . 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 2250	. . . . 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 2238	. . . 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 3326	. . 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 12863	. . . . . . . 8 |- ( ( S e. V /\ B e. _V /\ D e. X ) -> ( S sSet <. B , D >. ) = ( ( S |` ( _V \ { B } ) ) u. { <. B , D >. } ) )
36	34, 35	mp3an2 1338	. . . . . . 7 |- ( ( S e. V /\ D e. X ) -> ( S sSet <. B , D >. ) = ( ( S |` ( _V \ { B } ) ) u. { <. B , D >. } ) )
37	36	reseq1d 4958	. . . . . 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 4973	. . . . . 6 |- ( ( ( S |` ( _V \ { B } ) ) u. { <. B , D >. } ) |` ( _V \ { A } ) ) = ( ( ( S |` ( _V \ { B } ) ) |` ( _V \ { A } ) ) u. ( { <. B , D >. } |` ( _V \ { A } ) ) )
40		elex 2783	. . . . . . . . . . 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 4707	. . . . . . . . . 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 4272	. . . . . . . . . . 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 4778	. . . . . . . . . 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 5154	. . . . . . . . . 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 3215	. . . . . . . . . . 11 |- { A } C_ _V
52		ssv 3215	. . . . . . . . . . 11 |- { B } C_ _V
53		ssconb 3306	. . . . . . . . . . 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 3229	. . . . . . . 8 |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> dom { <. B , D >. } C_ ( _V \ { A } ) )
57		relssres 4997	. . . . . . . 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 3327	. . . . . 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 2250	. . . . 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 2238	. . . 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 3326	. . 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 2264	. 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 12864	. . . . 5 |- ( ( S e. V /\ A e. _V /\ C e. W ) -> ( S sSet <. A , C >. ) e. _V )
65	6, 64	mp3an2 1338	. . . 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 531	. . 3 |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> D e. X )
69		setsvala 12863	. . 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 1250	. 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 12864	. . . . 5 |- ( ( S e. V /\ B e. _V /\ D e. X ) -> ( S sSet <. B , D >. ) e. _V )
72	34, 71	mp3an2 1338	. . . 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 529	. . 3 |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> C e. W )
76		setsvala 12863	. . 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 1250	. 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 2248	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 1373   e. wcel 2176   =/= wne 2376   _Vcvv 2772   \ cdif 3163   u. cun 3164   i^i cin 3165   C_ wss 3166   (/)c0 3460   {csn 3633   <.cop 3636   X. cxp 4673   dom cdm 4675   |` cres 4677   Rel wrel 4680  (class class class)co 5944   sSet csts 12830

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 615  ax-in2 616  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-13 2178  ax-14 2179  ax-ext 2187  ax-sep 4162  ax-pow 4218  ax-pr 4253  ax-un 4480  ax-setind 4585

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1484  df-sb 1786  df-eu 2057  df-mo 2058  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ne 2377  df-ral 2489  df-rex 2490  df-rab 2493  df-v 2774  df-sbc 2999  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3461  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4045  df-opab 4106  df-id 4340  df-xp 4681  df-rel 4682  df-cnv 4683  df-co 4684  df-dm 4685  df-res 4687  df-iota 5232  df-fun 5273  df-fv 5279  df-ov 5947  df-oprab 5948  df-mpo 5949  df-sets 12839

This theorem is referenced by:  setscomd  12873