Metamath Proof Explorer

Theorem summolem2

Description: Lemma for summo . (Contributed by Mario Carneiro, 3-Apr-2014)

Ref Expression
Hypotheses summo.1 ⊢ 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
summo.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
summo.3 ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 )
Assertion summolem2 ( ( 𝜑 ∧ ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ) → ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) → 𝑥 = 𝑦 ) )

Proof

Step Hyp Ref Expression
1 summo.1 ⊢ 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
2 summo.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
3 summo.3 ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 )
4 fveq2 ⊢ ( 𝑚 = 𝑗 → ( ℤ≥ ‘ 𝑚 ) = ( ℤ≥ ‘ 𝑗 ) )
5 4 sseq2d ⊢ ( 𝑚 = 𝑗 → ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ↔ 𝐴 ⊆ ( ℤ≥ ‘ 𝑗 ) ) )
6 seqeq1 ⊢ ( 𝑚 = 𝑗 → seq 𝑚 ( + , 𝐹 ) = seq 𝑗 ( + , 𝐹 ) )
7 6 breq1d ⊢ ( 𝑚 = 𝑗 → ( seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ↔ seq 𝑗 ( + , 𝐹 ) ⇝ 𝑥 ) )
8 5 7 anbi12d ⊢ ( 𝑚 = 𝑗 → ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ↔ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑗 ) ∧ seq 𝑗 ( + , 𝐹 ) ⇝ 𝑥 ) ) )
9 8 cbvrexvw ⊢ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ↔ ∃ 𝑗 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑗 ) ∧ seq 𝑗 ( + , 𝐹 ) ⇝ 𝑥 ) )
10 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑗 ) ∧ seq 𝑗 ( + , 𝐹 ) ⇝ 𝑥 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ) → seq 𝑗 ( + , 𝐹 ) ⇝ 𝑥 )
11 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑗 ) ∧ seq 𝑗 ( + , 𝐹 ) ⇝ 𝑥 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ) → 𝐴 ⊆ ( ℤ≥ ‘ 𝑗 ) )
12 uzssz ⊢ ( ℤ≥ ‘ 𝑗 ) ⊆ ℤ
13 zssre ⊢ ℤ ⊆ ℝ
14 12 13 sstri ⊢ ( ℤ≥ ‘ 𝑗 ) ⊆ ℝ
15 11 14 sstrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑗 ) ∧ seq 𝑗 ( + , 𝐹 ) ⇝ 𝑥 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ) → 𝐴 ⊆ ℝ )
16 ltso ⊢ < Or ℝ
17 soss ⊢ ( 𝐴 ⊆ ℝ → ( < Or ℝ → < Or 𝐴 ) )
18 15 16 17 mpisyl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑗 ) ∧ seq 𝑗 ( + , 𝐹 ) ⇝ 𝑥 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ) → < Or 𝐴 )
19 fzfi ⊢ ( 1 ... 𝑚 ) ∈ Fin
20 ovex ⊢ ( 1 ... 𝑚 ) ∈ V
21 20 f1oen ⊢ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 → ( 1 ... 𝑚 ) ≈ 𝐴 )
22 21 ad2antll ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑗 ) ∧ seq 𝑗 ( + , 𝐹 ) ⇝ 𝑥 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ) → ( 1 ... 𝑚 ) ≈ 𝐴 )
23 22 ensymd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑗 ) ∧ seq 𝑗 ( + , 𝐹 ) ⇝ 𝑥 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ) → 𝐴 ≈ ( 1 ... 𝑚 ) )
24 enfii ⊢ ( ( ( 1 ... 𝑚 ) ∈ Fin ∧ 𝐴 ≈ ( 1 ... 𝑚 ) ) → 𝐴 ∈ Fin )
25 19 23 24 sylancr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑗 ) ∧ seq 𝑗 ( + , 𝐹 ) ⇝ 𝑥 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ) → 𝐴 ∈ Fin )
26 fz1iso ⊢ ( ( < Or 𝐴 ∧ 𝐴 ∈ Fin ) → ∃ 𝑔 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) )
27 18 25 26 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑗 ) ∧ seq 𝑗 ( + , 𝐹 ) ⇝ 𝑥 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ) → ∃ 𝑔 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) )
28 2 ad5ant15 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑗 ) ∧ seq 𝑗 ( + , 𝐹 ) ⇝ 𝑥 ) ) ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) ) ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
29 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) = ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 )
30 simprll ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑗 ) ∧ seq 𝑗 ( + , 𝐹 ) ⇝ 𝑥 ) ) ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) ) ) → 𝑚 ∈ ℕ )
31 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑗 ) ∧ seq 𝑗 ( + , 𝐹 ) ⇝ 𝑥 ) ) ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) ) ) → 𝑗 ∈ ℤ )
32 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑗 ) ∧ seq 𝑗 ( + , 𝐹 ) ⇝ 𝑥 ) ) ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) ) ) → 𝐴 ⊆ ( ℤ≥ ‘ 𝑗 ) )
33 simprlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑗 ) ∧ seq 𝑗 ( + , 𝐹 ) ⇝ 𝑥 ) ) ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) ) ) → 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 )
34 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑗 ) ∧ seq 𝑗 ( + , 𝐹 ) ⇝ 𝑥 ) ) ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) ) ) → 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) )
35 1 28 3 29 30 31 32 33 34 summolem2a ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑗 ) ∧ seq 𝑗 ( + , 𝐹 ) ⇝ 𝑥 ) ) ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) ) ) → seq 𝑗 ( + , 𝐹 ) ⇝ ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) )
36 35 expr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑗 ) ∧ seq 𝑗 ( + , 𝐹 ) ⇝ 𝑥 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ) → ( 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) → seq 𝑗 ( + , 𝐹 ) ⇝ ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) )
37 36 exlimdv ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑗 ) ∧ seq 𝑗 ( + , 𝐹 ) ⇝ 𝑥 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ) → ( ∃ 𝑔 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) → seq 𝑗 ( + , 𝐹 ) ⇝ ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) )
38 27 37 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑗 ) ∧ seq 𝑗 ( + , 𝐹 ) ⇝ 𝑥 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ) → seq 𝑗 ( + , 𝐹 ) ⇝ ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) )
39 climuni ⊢ ( ( seq 𝑗 ( + , 𝐹 ) ⇝ 𝑥 ∧ seq 𝑗 ( + , 𝐹 ) ⇝ ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) → 𝑥 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) )
40 10 38 39 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑗 ) ∧ seq 𝑗 ( + , 𝐹 ) ⇝ 𝑥 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ) → 𝑥 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) )
41 40 anassrs ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑗 ) ∧ seq 𝑗 ( + , 𝐹 ) ⇝ 𝑥 ) ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) → 𝑥 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) )
42 eqeq2 ⊢ ( 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) → ( 𝑥 = 𝑦 ↔ 𝑥 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) )
43 41 42 syl5ibrcom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑗 ) ∧ seq 𝑗 ( + , 𝐹 ) ⇝ 𝑥 ) ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) → ( 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) → 𝑥 = 𝑦 ) )
44 43 expimpd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑗 ) ∧ seq 𝑗 ( + , 𝐹 ) ⇝ 𝑥 ) ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) → 𝑥 = 𝑦 ) )
45 44 exlimdv ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑗 ) ∧ seq 𝑗 ( + , 𝐹 ) ⇝ 𝑥 ) ) ∧ 𝑚 ∈ ℕ ) → ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) → 𝑥 = 𝑦 ) )
46 45 rexlimdva ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑗 ) ∧ seq 𝑗 ( + , 𝐹 ) ⇝ 𝑥 ) ) → ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) → 𝑥 = 𝑦 ) )
47 46 r19.29an ⊢ ( ( 𝜑 ∧ ∃ 𝑗 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑗 ) ∧ seq 𝑗 ( + , 𝐹 ) ⇝ 𝑥 ) ) → ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) → 𝑥 = 𝑦 ) )
48 9 47 sylan2b ⊢ ( ( 𝜑 ∧ ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ) → ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) → 𝑥 = 𝑦 ) )