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∩Brepr⁡SM↔c∈Arepr⁡SM∧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↔cFn0..^S∧ran⁡c⊆B
6 ffn ⊢c:0..^S⟶A→cFn0..^S
7 6 adantl ⊢φ∧c:0..^S⟶A→cFn0..^S
8 7 biantrurd ⊢φ∧c:0..^S⟶A→ran⁡c⊆B↔cFn0..^S∧ran⁡c⊆B
9 8 bicomd ⊢φ∧c:0..^S⟶A→cFn0..^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∩B0..^S↔c:0..^S⟶A∩B
20 17 18 19 sylancl ⊢φ→c∈A∩B0..^S↔c:0..^S⟶A∩B
21 elmapg ⊢A∈V∧0..^S∈V→c∈A0..^S↔c:0..^S⟶A
22 15 18 21 sylancl ⊢φ→c∈A0..^S↔c:0..^S⟶A
23 22 anbi1d ⊢φ→c∈A0..^S∧ran⁡c⊆B↔c:0..^S⟶A∧ran⁡c⊆B
24 12 20 23 3bitr4d ⊢φ→c∈A∩B0..^S↔c∈A0..^S∧ran⁡c⊆B
25 24 anbi1d ⊢φ→c∈A∩B0..^S∧∑a∈0..^Sc⁡a=M↔c∈A0..^S∧ran⁡c⊆B∧∑a∈0..^Sc⁡a=M
26 inss1 ⊢A∩B⊆A
27 26 1 sstrid ⊢φ→A∩B⊆ℕ
28 27 2 3 reprval ⊢φ→A∩Brepr⁡SM=c∈A∩B0..^S|∑a∈0..^Sc⁡a=M
29 28 eleq2d ⊢φ→c∈A∩Brepr⁡SM↔c∈c∈A∩B0..^S|∑a∈0..^Sc⁡a=M
30 rabid ⊢c∈c∈A∩B0..^S|∑a∈0..^Sc⁡a=M↔c∈A∩B0..^S∧∑a∈0..^Sc⁡a=M
31 29 30 bitrdi ⊢φ→c∈A∩Brepr⁡SM↔c∈A∩B0..^S∧∑a∈0..^Sc⁡a=M
32 1 2 3 reprval ⊢φ→Arepr⁡SM=c∈A0..^S|∑a∈0..^Sc⁡a=M
33 32 eleq2d ⊢φ→c∈Arepr⁡SM↔c∈c∈A0..^S|∑a∈0..^Sc⁡a=M
34 rabid ⊢c∈c∈A0..^S|∑a∈0..^Sc⁡a=M↔c∈A0..^S∧∑a∈0..^Sc⁡a=M
35 33 34 bitrdi ⊢φ→c∈Arepr⁡SM↔c∈A0..^S∧∑a∈0..^Sc⁡a=M
36 35 anbi1d ⊢φ→c∈Arepr⁡SM∧ran⁡c⊆B↔c∈A0..^S∧∑a∈0..^Sc⁡a=M∧ran⁡c⊆B
37 an32 ⊢c∈A0..^S∧∑a∈0..^Sc⁡a=M∧ran⁡c⊆B↔c∈A0..^S∧ran⁡c⊆B∧∑a∈0..^Sc⁡a=M
38 36 37 bitrdi ⊢φ→c∈Arepr⁡SM∧ran⁡c⊆B↔c∈A0..^S∧ran⁡c⊆B∧∑a∈0..^Sc⁡a=M
39 25 31 38 3bitr4d ⊢φ→c∈A∩Brepr⁡SM↔c∈Arepr⁡SM∧ran⁡c⊆B