Metamath Proof Explorer

Theorem reprinrn

Description: Representations with term in an intersection. (Contributed by Thierry Arnoux, 11-Dec-2021)

Ref Expression
Hypotheses reprval.a ⊢ φ → A ⊆ ℕ
reprval.m ⊢ φ → M ∈ ℤ
reprval.s ⊢ φ → S ∈ ℕ 0
Assertion reprinrn ⊢ φ → c ∈ A ∩ B repr ⁡ S M ↔ c ∈ A repr ⁡ S M ∧ ran ⁡ c ⊆ B

Proof

Step Hyp Ref Expression
1 reprval.a ⊢ φ → A ⊆ ℕ
2 reprval.m ⊢ φ → M ∈ ℤ
3 reprval.s ⊢ φ → S ∈ ℕ 0
4 fin ⊢ c : 0 ..^ S ⟶ A ∩ B ↔ c : 0 ..^ S ⟶ A ∧ c : 0 ..^ S ⟶ B
5 df-f ⊢ c : 0 ..^ S ⟶ B ↔ c Fn 0 ..^ S ∧ ran ⁡ c ⊆ B
6 ffn ⊢ c : 0 ..^ S ⟶ A → c Fn 0 ..^ S
7 6 adantl ⊢ φ ∧ c : 0 ..^ S ⟶ A → c Fn 0 ..^ S
8 7 biantrurd ⊢ φ ∧ c : 0 ..^ S ⟶ A → ran ⁡ c ⊆ B ↔ c Fn 0 ..^ S ∧ ran ⁡ c ⊆ B
9 8 bicomd ⊢ φ ∧ c : 0 ..^ S ⟶ A → c Fn 0 ..^ S ∧ ran ⁡ c ⊆ B ↔ ran ⁡ c ⊆ B
10 5 9 bitrid ⊢ φ ∧ c : 0 ..^ S ⟶ A → c : 0 ..^ S ⟶ B ↔ ran ⁡ c ⊆ B
11 10 pm5.32da ⊢ φ → c : 0 ..^ S ⟶ A ∧ c : 0 ..^ S ⟶ B ↔ c : 0 ..^ S ⟶ A ∧ ran ⁡ c ⊆ B
12 4 11 bitrid ⊢ φ → c : 0 ..^ S ⟶ A ∩ B ↔ c : 0 ..^ S ⟶ A ∧ ran ⁡ c ⊆ B
13 nnex ⊢ ℕ ∈ V
14 13 a1i ⊢ φ → ℕ ∈ V
15 14 1 ssexd ⊢ φ → A ∈ V
16 inex1g ⊢ A ∈ V → A ∩ B ∈ V
17 15 16 syl ⊢ φ → A ∩ B ∈ V
18 ovex ⊢ 0 ..^ S ∈ V
19 elmapg ⊢ A ∩ B ∈ V ∧ 0 ..^ S ∈ V → c ∈ A ∩ B 0 ..^ S ↔ c : 0 ..^ S ⟶ A ∩ B
20 17 18 19 sylancl ⊢ φ → c ∈ A ∩ B 0 ..^ S ↔ c : 0 ..^ S ⟶ A ∩ B
21 elmapg ⊢ A ∈ V ∧ 0 ..^ S ∈ V → c ∈ A 0 ..^ S ↔ c : 0 ..^ S ⟶ A
22 15 18 21 sylancl ⊢ φ → c ∈ A 0 ..^ S ↔ c : 0 ..^ S ⟶ A
23 22 anbi1d ⊢ φ → c ∈ A 0 ..^ S ∧ ran ⁡ c ⊆ B ↔ c : 0 ..^ S ⟶ A ∧ ran ⁡ c ⊆ B
24 12 20 23 3bitr4d ⊢ φ → c ∈ A ∩ B 0 ..^ S ↔ c ∈ A 0 ..^ S ∧ ran ⁡ c ⊆ B
25 24 anbi1d ⊢ φ → c ∈ A ∩ B 0 ..^ S ∧ ∑ a ∈ 0 ..^ S c ⁡ a = M ↔ c ∈ A 0 ..^ S ∧ ran ⁡ c ⊆ B ∧ ∑ a ∈ 0 ..^ S c ⁡ a = M
26 inss1 ⊢ A ∩ B ⊆ A
27 26 1 sstrid ⊢ φ → A ∩ B ⊆ ℕ
28 27 2 3 reprval ⊢ φ → A ∩ B repr ⁡ S M = c ∈ A ∩ B 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = M
29 28 eleq2d ⊢ φ → c ∈ A ∩ B repr ⁡ S M ↔ c ∈ c ∈ A ∩ B 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = M
30 rabid ⊢ c ∈ c ∈ A ∩ B 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = M ↔ c ∈ A ∩ B 0 ..^ S ∧ ∑ a ∈ 0 ..^ S c ⁡ a = M
31 29 30 bitrdi ⊢ φ → c ∈ A ∩ B repr ⁡ S M ↔ c ∈ A ∩ B 0 ..^ S ∧ ∑ a ∈ 0 ..^ S c ⁡ a = M
32 1 2 3 reprval ⊢ φ → A repr ⁡ S M = c ∈ A 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = M
33 32 eleq2d ⊢ φ → c ∈ A repr ⁡ S M ↔ c ∈ c ∈ A 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = M
34 rabid ⊢ c ∈ c ∈ A 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = M ↔ c ∈ A 0 ..^ S ∧ ∑ a ∈ 0 ..^ S c ⁡ a = M
35 33 34 bitrdi ⊢ φ → c ∈ A repr ⁡ S M ↔ c ∈ A 0 ..^ S ∧ ∑ a ∈ 0 ..^ S c ⁡ a = M
36 35 anbi1d ⊢ φ → c ∈ A repr ⁡ S M ∧ ran ⁡ c ⊆ B ↔ c ∈ A 0 ..^ S ∧ ∑ a ∈ 0 ..^ S c ⁡ a = M ∧ ran ⁡ c ⊆ B
37 an32 ⊢ c ∈ A 0 ..^ S ∧ ∑ a ∈ 0 ..^ S c ⁡ a = M ∧ ran ⁡ c ⊆ B ↔ c ∈ A 0 ..^ S ∧ ran ⁡ c ⊆ B ∧ ∑ a ∈ 0 ..^ S c ⁡ a = M
38 36 37 bitrdi ⊢ φ → c ∈ A repr ⁡ S M ∧ ran ⁡ c ⊆ B ↔ c ∈ A 0 ..^ S ∧ ran ⁡ c ⊆ B ∧ ∑ a ∈ 0 ..^ S c ⁡ a = M
39 25 31 38 3bitr4d ⊢ φ → c ∈ A ∩ B repr ⁡ S M ↔ c ∈ A repr ⁡ S M ∧ ran ⁡ c ⊆ B