Metamath Proof Explorer

Theorem reprdifc

Description: Express the representations as a sum of integers in a difference of sets using conditions on each of the indices. (Contributed by Thierry Arnoux, 27-Dec-2021)

Ref Expression
Hypotheses reprdifc.c ⊢ 𝐶 = { 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∣ ¬ ( 𝑐 ‘ 𝑥 ) ∈ 𝐵 }
reprdifc.a ⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
reprdifc.b ⊢ ( 𝜑 → 𝐵 ⊆ ℕ )
reprdifc.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
reprdifc.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
Assertion reprdifc ( 𝜑 → ( ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∖ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ) = ∪ 𝑥 ∈ ( 0 ..^ 𝑆 ) 𝐶 )

Proof

Step Hyp Ref Expression
1 reprdifc.c ⊢ 𝐶 = { 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∣ ¬ ( 𝑐 ‘ 𝑥 ) ∈ 𝐵 }
2 reprdifc.a ⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
3 reprdifc.b ⊢ ( 𝜑 → 𝐵 ⊆ ℕ )
4 reprdifc.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
5 reprdifc.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
6 nfv ⊢ Ⅎ 𝑑 𝜑
7 nfrab1 ⊢ Ⅎ 𝑑 { 𝑑 ∈ ( ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∖ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 }
8 nfcv ⊢ Ⅎ 𝑑 ∪ 𝑥 ∈ ( 0 ..^ 𝑆 ) { 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∣ ¬ ( 𝑐 ‘ 𝑥 ) ∈ 𝐵 }
9 4 nn0zd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
10 2 9 5 reprval ⊢ ( 𝜑 → ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) = { 𝑑 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 } )
11 10 eleq2d ⊢ ( 𝜑 → ( 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ↔ 𝑑 ∈ { 𝑑 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 } ) )
12 rabid ⊢ ( 𝑑 ∈ { 𝑑 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 } ↔ ( 𝑑 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 ) )
13 11 12 bitrdi ⊢ ( 𝜑 → ( 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ↔ ( 𝑑 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 ) ) )
14 13 anbi1d ⊢ ( 𝜑 → ( ( 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ¬ 𝑑 ∈ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ) ↔ ( ( 𝑑 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 ) ∧ ¬ 𝑑 ∈ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ) ) )
15 eldif ⊢ ( 𝑑 ∈ ( ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∖ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ) ↔ ( 𝑑 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∧ ¬ 𝑑 ∈ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ) )
16 15 anbi1i ⊢ ( ( 𝑑 ∈ ( ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∖ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 ) ↔ ( ( 𝑑 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∧ ¬ 𝑑 ∈ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 ) )
17 an32 ⊢ ( ( ( 𝑑 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∧ ¬ 𝑑 ∈ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 ) ↔ ( ( 𝑑 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 ) ∧ ¬ 𝑑 ∈ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ) )
18 16 17 bitri ⊢ ( ( 𝑑 ∈ ( ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∖ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 ) ↔ ( ( 𝑑 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 ) ∧ ¬ 𝑑 ∈ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ) )
19 18 a1i ⊢ ( 𝜑 → ( ( 𝑑 ∈ ( ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∖ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 ) ↔ ( ( 𝑑 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 ) ∧ ¬ 𝑑 ∈ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ) ) )
20 14 19 bitr4d ⊢ ( 𝜑 → ( ( 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ¬ 𝑑 ∈ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ) ↔ ( 𝑑 ∈ ( ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∖ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 ) ) )
21 nnex ⊢ ℕ ∈ V
22 21 a1i ⊢ ( 𝜑 → ℕ ∈ V )
23 22 3 ssexd ⊢ ( 𝜑 → 𝐵 ∈ V )
24 ovexd ⊢ ( 𝜑 → ( 0 ..^ 𝑆 ) ∈ V )
25 elmapg ⊢ ( ( 𝐵 ∈ V ∧ ( 0 ..^ 𝑆 ) ∈ V ) → ( 𝑑 ∈ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ↔ 𝑑 : ( 0 ..^ 𝑆 ) ⟶ 𝐵 ) )
26 23 24 25 syl2anc ⊢ ( 𝜑 → ( 𝑑 ∈ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ↔ 𝑑 : ( 0 ..^ 𝑆 ) ⟶ 𝐵 ) )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) → ( 𝑑 ∈ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ↔ 𝑑 : ( 0 ..^ 𝑆 ) ⟶ 𝐵 ) )
28 ffnfv ⊢ ( 𝑑 : ( 0 ..^ 𝑆 ) ⟶ 𝐵 ↔ ( 𝑑 Fn ( 0 ..^ 𝑆 ) ∧ ∀ 𝑥 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑥 ) ∈ 𝐵 ) )
29 2 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) → 𝐴 ⊆ ℕ )
30 9 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) → 𝑀 ∈ ℤ )
31 5 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) → 𝑆 ∈ ℕ0 )
32 simpr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) → 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) )
33 29 30 31 32 reprf ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) → 𝑑 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 )
34 33 ffnd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) → 𝑑 Fn ( 0 ..^ 𝑆 ) )
35 34 biantrurd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) → ( ∀ 𝑥 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑥 ) ∈ 𝐵 ↔ ( 𝑑 Fn ( 0 ..^ 𝑆 ) ∧ ∀ 𝑥 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑥 ) ∈ 𝐵 ) ) )
36 28 35 bitr4id ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) → ( 𝑑 : ( 0 ..^ 𝑆 ) ⟶ 𝐵 ↔ ∀ 𝑥 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑥 ) ∈ 𝐵 ) )
37 27 36 bitrd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) → ( 𝑑 ∈ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ↔ ∀ 𝑥 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑥 ) ∈ 𝐵 ) )
38 37 notbid ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) → ( ¬ 𝑑 ∈ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ↔ ¬ ∀ 𝑥 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑥 ) ∈ 𝐵 ) )
39 rexnal ⊢ ( ∃ 𝑥 ∈ ( 0 ..^ 𝑆 ) ¬ ( 𝑑 ‘ 𝑥 ) ∈ 𝐵 ↔ ¬ ∀ 𝑥 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑥 ) ∈ 𝐵 )
40 38 39 bitr4di ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ) → ( ¬ 𝑑 ∈ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ↔ ∃ 𝑥 ∈ ( 0 ..^ 𝑆 ) ¬ ( 𝑑 ‘ 𝑥 ) ∈ 𝐵 ) )
41 40 pm5.32da ⊢ ( 𝜑 → ( ( 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ¬ 𝑑 ∈ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ) ↔ ( 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ∃ 𝑥 ∈ ( 0 ..^ 𝑆 ) ¬ ( 𝑑 ‘ 𝑥 ) ∈ 𝐵 ) ) )
42 20 41 bitr3d ⊢ ( 𝜑 → ( ( 𝑑 ∈ ( ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∖ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 ) ↔ ( 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ∃ 𝑥 ∈ ( 0 ..^ 𝑆 ) ¬ ( 𝑑 ‘ 𝑥 ) ∈ 𝐵 ) ) )
43 fveq1 ⊢ ( 𝑐 = 𝑑 → ( 𝑐 ‘ 𝑥 ) = ( 𝑑 ‘ 𝑥 ) )
44 43 eleq1d ⊢ ( 𝑐 = 𝑑 → ( ( 𝑐 ‘ 𝑥 ) ∈ 𝐵 ↔ ( 𝑑 ‘ 𝑥 ) ∈ 𝐵 ) )
45 44 notbid ⊢ ( 𝑐 = 𝑑 → ( ¬ ( 𝑐 ‘ 𝑥 ) ∈ 𝐵 ↔ ¬ ( 𝑑 ‘ 𝑥 ) ∈ 𝐵 ) )
46 45 elrab ⊢ ( 𝑑 ∈ { 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∣ ¬ ( 𝑐 ‘ 𝑥 ) ∈ 𝐵 } ↔ ( 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ¬ ( 𝑑 ‘ 𝑥 ) ∈ 𝐵 ) )
47 46 rexbii ⊢ ( ∃ 𝑥 ∈ ( 0 ..^ 𝑆 ) 𝑑 ∈ { 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∣ ¬ ( 𝑐 ‘ 𝑥 ) ∈ 𝐵 } ↔ ∃ 𝑥 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ¬ ( 𝑑 ‘ 𝑥 ) ∈ 𝐵 ) )
48 r19.42v ⊢ ( ∃ 𝑥 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ¬ ( 𝑑 ‘ 𝑥 ) ∈ 𝐵 ) ↔ ( 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ∃ 𝑥 ∈ ( 0 ..^ 𝑆 ) ¬ ( 𝑑 ‘ 𝑥 ) ∈ 𝐵 ) )
49 47 48 bitri ⊢ ( ∃ 𝑥 ∈ ( 0 ..^ 𝑆 ) 𝑑 ∈ { 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∣ ¬ ( 𝑐 ‘ 𝑥 ) ∈ 𝐵 } ↔ ( 𝑑 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ∃ 𝑥 ∈ ( 0 ..^ 𝑆 ) ¬ ( 𝑑 ‘ 𝑥 ) ∈ 𝐵 ) )
50 42 49 bitr4di ⊢ ( 𝜑 → ( ( 𝑑 ∈ ( ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∖ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 ) ↔ ∃ 𝑥 ∈ ( 0 ..^ 𝑆 ) 𝑑 ∈ { 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∣ ¬ ( 𝑐 ‘ 𝑥 ) ∈ 𝐵 } ) )
51 rabid ⊢ ( 𝑑 ∈ { 𝑑 ∈ ( ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∖ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 } ↔ ( 𝑑 ∈ ( ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∖ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 ) )
52 eliun ⊢ ( 𝑑 ∈ ∪ 𝑥 ∈ ( 0 ..^ 𝑆 ) { 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∣ ¬ ( 𝑐 ‘ 𝑥 ) ∈ 𝐵 } ↔ ∃ 𝑥 ∈ ( 0 ..^ 𝑆 ) 𝑑 ∈ { 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∣ ¬ ( 𝑐 ‘ 𝑥 ) ∈ 𝐵 } )
53 50 51 52 3bitr4g ⊢ ( 𝜑 → ( 𝑑 ∈ { 𝑑 ∈ ( ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∖ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 } ↔ 𝑑 ∈ ∪ 𝑥 ∈ ( 0 ..^ 𝑆 ) { 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∣ ¬ ( 𝑐 ‘ 𝑥 ) ∈ 𝐵 } ) )
54 6 7 8 53 eqrd ⊢ ( 𝜑 → { 𝑑 ∈ ( ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∖ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 } = ∪ 𝑥 ∈ ( 0 ..^ 𝑆 ) { 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∣ ¬ ( 𝑐 ‘ 𝑥 ) ∈ 𝐵 } )
55 3 9 5 reprval ⊢ ( 𝜑 → ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) = { 𝑑 ∈ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 } )
56 10 55 difeq12d ⊢ ( 𝜑 → ( ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∖ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ) = ( { 𝑑 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 } ∖ { 𝑑 ∈ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 } ) )
57 difrab2 ⊢ ( { 𝑑 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 } ∖ { 𝑑 ∈ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 } ) = { 𝑑 ∈ ( ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∖ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 }
58 56 57 eqtrdi ⊢ ( 𝜑 → ( ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∖ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ) = { 𝑑 ∈ ( ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∖ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑑 ‘ 𝑎 ) = 𝑀 } )
59 1 a1i ⊢ ( 𝜑 → 𝐶 = { 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∣ ¬ ( 𝑐 ‘ 𝑥 ) ∈ 𝐵 } )
60 59 iuneq2d ⊢ ( 𝜑 → ∪ 𝑥 ∈ ( 0 ..^ 𝑆 ) 𝐶 = ∪ 𝑥 ∈ ( 0 ..^ 𝑆 ) { 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∣ ¬ ( 𝑐 ‘ 𝑥 ) ∈ 𝐵 } )
61 54 58 60 3eqtr4d ⊢ ( 𝜑 → ( ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∖ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ) = ∪ 𝑥 ∈ ( 0 ..^ 𝑆 ) 𝐶 )