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 ( · , 𝐺 ) ‘ 𝑚 ) ) → 𝑥 = 𝑧 ) )