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 V
setscom.2 B V
Assertion setscom S V A B C W D X S sSet A C sSet B D = S sSet B D sSet A C

Proof

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