Metamath Proof Explorer

Theorem prodmolem2

Description: Lemma for prodmo . (Contributed by Scott Fenton, 4-Dec-2017)

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

Proof

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