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 ⊢ 𝐴 ∈ V
setscom.2 ⊢ 𝐵 ∈ V
Assertion setscom ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → ( ( 𝑆 sSet ⟨ 𝐴 , 𝐶 ⟩ ) sSet ⟨ 𝐵 , 𝐷 ⟩ ) = ( ( 𝑆 sSet ⟨ 𝐵 , 𝐷 ⟩ ) sSet ⟨ 𝐴 , 𝐶 ⟩ ) )

Proof

Step Hyp Ref Expression
1 setscom.1 ⊢ 𝐴 ∈ V
2 setscom.2 ⊢ 𝐵 ∈ V
3 rescom ⊢ ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ↾ ( V ∖ { 𝐵 } ) ) = ( ( 𝑆 ↾ ( V ∖ { 𝐵 } ) ) ↾ ( V ∖ { 𝐴 } ) )
4 3 uneq1i ⊢ ( ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ↾ ( V ∖ { 𝐵 } ) ) ∪ { ⟨ 𝐴 , 𝐶 ⟩ } ) = ( ( ( 𝑆 ↾ ( V ∖ { 𝐵 } ) ) ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐶 ⟩ } )
5 4 uneq1i ⊢ ( ( ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ↾ ( V ∖ { 𝐵 } ) ) ∪ { ⟨ 𝐴 , 𝐶 ⟩ } ) ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) = ( ( ( ( 𝑆 ↾ ( V ∖ { 𝐵 } ) ) ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐶 ⟩ } ) ∪ { ⟨ 𝐵 , 𝐷 ⟩ } )
6 un23 ⊢ ( ( ( ( 𝑆 ↾ ( V ∖ { 𝐵 } ) ) ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐶 ⟩ } ) ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) = ( ( ( ( 𝑆 ↾ ( V ∖ { 𝐵 } ) ) ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) ∪ { ⟨ 𝐴 , 𝐶 ⟩ } )
7 5 6 eqtri ⊢ ( ( ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ↾ ( V ∖ { 𝐵 } ) ) ∪ { ⟨ 𝐴 , 𝐶 ⟩ } ) ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) = ( ( ( ( 𝑆 ↾ ( V ∖ { 𝐵 } ) ) ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) ∪ { ⟨ 𝐴 , 𝐶 ⟩ } )
8 setsval ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝑆 sSet ⟨ 𝐴 , 𝐶 ⟩ ) = ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐶 ⟩ } ) )
9 8 ad2ant2r ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → ( 𝑆 sSet ⟨ 𝐴 , 𝐶 ⟩ ) = ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐶 ⟩ } ) )
10 9 reseq1d ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → ( ( 𝑆 sSet ⟨ 𝐴 , 𝐶 ⟩ ) ↾ ( V ∖ { 𝐵 } ) ) = ( ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐶 ⟩ } ) ↾ ( V ∖ { 𝐵 } ) ) )
11 resundir ⊢ ( ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐶 ⟩ } ) ↾ ( V ∖ { 𝐵 } ) ) = ( ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ↾ ( V ∖ { 𝐵 } ) ) ∪ ( { ⟨ 𝐴 , 𝐶 ⟩ } ↾ ( V ∖ { 𝐵 } ) ) )
12 elex ⊢ ( 𝐶 ∈ 𝑊 → 𝐶 ∈ V )
13 12 ad2antrl ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → 𝐶 ∈ V )
14 opelxpi ⊢ ( ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) → ⟨ 𝐴 , 𝐶 ⟩ ∈ ( V × V ) )
15 1 13 14 sylancr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → ⟨ 𝐴 , 𝐶 ⟩ ∈ ( V × V ) )
16 opex ⊢ ⟨ 𝐴 , 𝐶 ⟩ ∈ V
17 16 relsn ⊢ ( Rel { ⟨ 𝐴 , 𝐶 ⟩ } ↔ ⟨ 𝐴 , 𝐶 ⟩ ∈ ( V × V ) )
18 15 17 sylibr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → Rel { ⟨ 𝐴 , 𝐶 ⟩ } )
19 dmsnopss ⊢ dom { ⟨ 𝐴 , 𝐶 ⟩ } ⊆ { 𝐴 }
20 disjsn2 ⊢ ( 𝐴 ≠ 𝐵 → ( { 𝐴 } ∩ { 𝐵 } ) = ∅ )
21 20 ad2antlr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → ( { 𝐴 } ∩ { 𝐵 } ) = ∅ )
22 disj2 ⊢ ( ( { 𝐴 } ∩ { 𝐵 } ) = ∅ ↔ { 𝐴 } ⊆ ( V ∖ { 𝐵 } ) )
23 21 22 sylib ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → { 𝐴 } ⊆ ( V ∖ { 𝐵 } ) )
24 19 23 sstrid ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → dom { ⟨ 𝐴 , 𝐶 ⟩ } ⊆ ( V ∖ { 𝐵 } ) )
25 relssres ⊢ ( ( Rel { ⟨ 𝐴 , 𝐶 ⟩ } ∧ dom { ⟨ 𝐴 , 𝐶 ⟩ } ⊆ ( V ∖ { 𝐵 } ) ) → ( { ⟨ 𝐴 , 𝐶 ⟩ } ↾ ( V ∖ { 𝐵 } ) ) = { ⟨ 𝐴 , 𝐶 ⟩ } )
26 18 24 25 syl2anc ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → ( { ⟨ 𝐴 , 𝐶 ⟩ } ↾ ( V ∖ { 𝐵 } ) ) = { ⟨ 𝐴 , 𝐶 ⟩ } )
27 26 uneq2d ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → ( ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ↾ ( V ∖ { 𝐵 } ) ) ∪ ( { ⟨ 𝐴 , 𝐶 ⟩ } ↾ ( V ∖ { 𝐵 } ) ) ) = ( ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ↾ ( V ∖ { 𝐵 } ) ) ∪ { ⟨ 𝐴 , 𝐶 ⟩ } ) )
28 11 27 eqtrid ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → ( ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐶 ⟩ } ) ↾ ( V ∖ { 𝐵 } ) ) = ( ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ↾ ( V ∖ { 𝐵 } ) ) ∪ { ⟨ 𝐴 , 𝐶 ⟩ } ) )
29 10 28 eqtrd ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → ( ( 𝑆 sSet ⟨ 𝐴 , 𝐶 ⟩ ) ↾ ( V ∖ { 𝐵 } ) ) = ( ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ↾ ( V ∖ { 𝐵 } ) ) ∪ { ⟨ 𝐴 , 𝐶 ⟩ } ) )
30 29 uneq1d ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → ( ( ( 𝑆 sSet ⟨ 𝐴 , 𝐶 ⟩ ) ↾ ( V ∖ { 𝐵 } ) ) ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) = ( ( ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ↾ ( V ∖ { 𝐵 } ) ) ∪ { ⟨ 𝐴 , 𝐶 ⟩ } ) ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) )
31 setsval ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐷 ∈ 𝑋 ) → ( 𝑆 sSet ⟨ 𝐵 , 𝐷 ⟩ ) = ( ( 𝑆 ↾ ( V ∖ { 𝐵 } ) ) ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) )
32 31 reseq1d ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐷 ∈ 𝑋 ) → ( ( 𝑆 sSet ⟨ 𝐵 , 𝐷 ⟩ ) ↾ ( V ∖ { 𝐴 } ) ) = ( ( ( 𝑆 ↾ ( V ∖ { 𝐵 } ) ) ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) ↾ ( V ∖ { 𝐴 } ) ) )
33 32 ad2ant2rl ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → ( ( 𝑆 sSet ⟨ 𝐵 , 𝐷 ⟩ ) ↾ ( V ∖ { 𝐴 } ) ) = ( ( ( 𝑆 ↾ ( V ∖ { 𝐵 } ) ) ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) ↾ ( V ∖ { 𝐴 } ) ) )
34 resundir ⊢ ( ( ( 𝑆 ↾ ( V ∖ { 𝐵 } ) ) ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) ↾ ( V ∖ { 𝐴 } ) ) = ( ( ( 𝑆 ↾ ( V ∖ { 𝐵 } ) ) ↾ ( V ∖ { 𝐴 } ) ) ∪ ( { ⟨ 𝐵 , 𝐷 ⟩ } ↾ ( V ∖ { 𝐴 } ) ) )
35 elex ⊢ ( 𝐷 ∈ 𝑋 → 𝐷 ∈ V )
36 35 ad2antll ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → 𝐷 ∈ V )
37 opelxpi ⊢ ( ( 𝐵 ∈ V ∧ 𝐷 ∈ V ) → ⟨ 𝐵 , 𝐷 ⟩ ∈ ( V × V ) )
38 2 36 37 sylancr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → ⟨ 𝐵 , 𝐷 ⟩ ∈ ( V × V ) )
39 opex ⊢ ⟨ 𝐵 , 𝐷 ⟩ ∈ V
40 39 relsn ⊢ ( Rel { ⟨ 𝐵 , 𝐷 ⟩ } ↔ ⟨ 𝐵 , 𝐷 ⟩ ∈ ( V × V ) )
41 38 40 sylibr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → Rel { ⟨ 𝐵 , 𝐷 ⟩ } )
42 dmsnopss ⊢ dom { ⟨ 𝐵 , 𝐷 ⟩ } ⊆ { 𝐵 }
43 ssv ⊢ { 𝐴 } ⊆ V
44 ssv ⊢ { 𝐵 } ⊆ V
45 ssconb ⊢ ( ( { 𝐴 } ⊆ V ∧ { 𝐵 } ⊆ V ) → ( { 𝐴 } ⊆ ( V ∖ { 𝐵 } ) ↔ { 𝐵 } ⊆ ( V ∖ { 𝐴 } ) ) )
46 43 44 45 mp2an ⊢ ( { 𝐴 } ⊆ ( V ∖ { 𝐵 } ) ↔ { 𝐵 } ⊆ ( V ∖ { 𝐴 } ) )
47 23 46 sylib ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → { 𝐵 } ⊆ ( V ∖ { 𝐴 } ) )
48 42 47 sstrid ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → dom { ⟨ 𝐵 , 𝐷 ⟩ } ⊆ ( V ∖ { 𝐴 } ) )
49 relssres ⊢ ( ( Rel { ⟨ 𝐵 , 𝐷 ⟩ } ∧ dom { ⟨ 𝐵 , 𝐷 ⟩ } ⊆ ( V ∖ { 𝐴 } ) ) → ( { ⟨ 𝐵 , 𝐷 ⟩ } ↾ ( V ∖ { 𝐴 } ) ) = { ⟨ 𝐵 , 𝐷 ⟩ } )
50 41 48 49 syl2anc ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → ( { ⟨ 𝐵 , 𝐷 ⟩ } ↾ ( V ∖ { 𝐴 } ) ) = { ⟨ 𝐵 , 𝐷 ⟩ } )
51 50 uneq2d ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → ( ( ( 𝑆 ↾ ( V ∖ { 𝐵 } ) ) ↾ ( V ∖ { 𝐴 } ) ) ∪ ( { ⟨ 𝐵 , 𝐷 ⟩ } ↾ ( V ∖ { 𝐴 } ) ) ) = ( ( ( 𝑆 ↾ ( V ∖ { 𝐵 } ) ) ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) )
52 34 51 eqtrid ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → ( ( ( 𝑆 ↾ ( V ∖ { 𝐵 } ) ) ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) ↾ ( V ∖ { 𝐴 } ) ) = ( ( ( 𝑆 ↾ ( V ∖ { 𝐵 } ) ) ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) )
53 33 52 eqtrd ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → ( ( 𝑆 sSet ⟨ 𝐵 , 𝐷 ⟩ ) ↾ ( V ∖ { 𝐴 } ) ) = ( ( ( 𝑆 ↾ ( V ∖ { 𝐵 } ) ) ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) )
54 53 uneq1d ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → ( ( ( 𝑆 sSet ⟨ 𝐵 , 𝐷 ⟩ ) ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐶 ⟩ } ) = ( ( ( ( 𝑆 ↾ ( V ∖ { 𝐵 } ) ) ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) ∪ { ⟨ 𝐴 , 𝐶 ⟩ } ) )
55 7 30 54 3eqtr4a ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → ( ( ( 𝑆 sSet ⟨ 𝐴 , 𝐶 ⟩ ) ↾ ( V ∖ { 𝐵 } ) ) ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) = ( ( ( 𝑆 sSet ⟨ 𝐵 , 𝐷 ⟩ ) ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐶 ⟩ } ) )
56 ovex ⊢ ( 𝑆 sSet ⟨ 𝐴 , 𝐶 ⟩ ) ∈ V
57 simprr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → 𝐷 ∈ 𝑋 )
58 setsval ⊢ ( ( ( 𝑆 sSet ⟨ 𝐴 , 𝐶 ⟩ ) ∈ V ∧ 𝐷 ∈ 𝑋 ) → ( ( 𝑆 sSet ⟨ 𝐴 , 𝐶 ⟩ ) sSet ⟨ 𝐵 , 𝐷 ⟩ ) = ( ( ( 𝑆 sSet ⟨ 𝐴 , 𝐶 ⟩ ) ↾ ( V ∖ { 𝐵 } ) ) ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) )
59 56 57 58 sylancr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → ( ( 𝑆 sSet ⟨ 𝐴 , 𝐶 ⟩ ) sSet ⟨ 𝐵 , 𝐷 ⟩ ) = ( ( ( 𝑆 sSet ⟨ 𝐴 , 𝐶 ⟩ ) ↾ ( V ∖ { 𝐵 } ) ) ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) )
60 ovex ⊢ ( 𝑆 sSet ⟨ 𝐵 , 𝐷 ⟩ ) ∈ V
61 simprl ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → 𝐶 ∈ 𝑊 )
62 setsval ⊢ ( ( ( 𝑆 sSet ⟨ 𝐵 , 𝐷 ⟩ ) ∈ V ∧ 𝐶 ∈ 𝑊 ) → ( ( 𝑆 sSet ⟨ 𝐵 , 𝐷 ⟩ ) sSet ⟨ 𝐴 , 𝐶 ⟩ ) = ( ( ( 𝑆 sSet ⟨ 𝐵 , 𝐷 ⟩ ) ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐶 ⟩ } ) )
63 60 61 62 sylancr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → ( ( 𝑆 sSet ⟨ 𝐵 , 𝐷 ⟩ ) sSet ⟨ 𝐴 , 𝐶 ⟩ ) = ( ( ( 𝑆 sSet ⟨ 𝐵 , 𝐷 ⟩ ) ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐶 ⟩ } ) )
64 55 59 63 3eqtr4d ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋 ) ) → ( ( 𝑆 sSet ⟨ 𝐴 , 𝐶 ⟩ ) sSet ⟨ 𝐵 , 𝐷 ⟩ ) = ( ( 𝑆 sSet ⟨ 𝐵 , 𝐷 ⟩ ) sSet ⟨ 𝐴 , 𝐶 ⟩ ) )