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 \in V$
	setscom.2	$⊢ B \in V$
Assertion	setscom	$⊢ ((S \in V \land A \neq B) \land (C \in W \land D \in X)) \to (S sSet ⟨A, C⟩) sSet ⟨B, D⟩ = (S sSet ⟨B, D⟩) sSet ⟨A, C⟩$

Proof

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

Metamath Proof Explorer

Theorem setscom

Proof