summolem2

	Ref	Expression
Hypotheses	summo.1	$⊢ F = (k \in ℤ ⟼ if (k \in A, B, 0))$
	summo.2	$⊢ (φ \land k \in A) \to B \in ℂ$
	summo.3	$⊢ G = (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)$
Assertion	summolem2	$⊢ (φ \land \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x)) \to (\exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ G) (m)) \to x = y)$

Proof

Step	Hyp	Ref	Expression
1		summo.1	$⊢ F = (k \in ℤ ⟼ if (k \in A, B, 0))$
2		summo.2	$⊢ (φ \land k \in A) \to B \in ℂ$
3		summo.3	$⊢ G = (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)$
4		fveq2	$⊢ m = j \to ℤ_{\geq m} = ℤ_{\geq j}$
5	4	sseq2d	$⊢ m = j \to (A \subseteq ℤ_{\geq m} \leftrightarrow A \subseteq ℤ_{\geq j})$
6		seqeq1	$⊢ m = j \to seq m (+ F) = seq j (+ F)$
7	6	breq1d	$⊢ m = j \to (seq m (+ F) ⇝ x \leftrightarrow seq j (+ F) ⇝ x)$
8	5 7	anbi12d	$⊢ m = j \to ((A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x) \leftrightarrow (A \subseteq ℤ_{\geq j} \land seq j (+ F) ⇝ x))$
9	8	cbvrexvw	$⊢ \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x) \leftrightarrow \exists j \in ℤ (A \subseteq ℤ_{\geq j} \land seq j (+ F) ⇝ x)$
10		simplrr	$⊢ (((φ \land j \in ℤ) \land (A \subseteq ℤ_{\geq j} \land seq j (+ F) ⇝ x)) \land (m \in ℕ \land f : (1 \dots m) \underset{1-1 onto}{⟶} A)) \to seq j (+ F) ⇝ x$
11		simplrl	$⊢ (((φ \land j \in ℤ) \land (A \subseteq ℤ_{\geq j} \land seq j (+ F) ⇝ x)) \land (m \in ℕ \land f : (1 \dots m) \underset{1-1 onto}{⟶} A)) \to A \subseteq ℤ_{\geq j}$
12		uzssz	$⊢ ℤ_{\geq j} \subseteq ℤ$
13		zssre	$⊢ ℤ \subseteq ℝ$
14	12 13	sstri	$⊢ ℤ_{\geq j} \subseteq ℝ$
15	11 14	sstrdi	$⊢ (((φ \land j \in ℤ) \land (A \subseteq ℤ_{\geq j} \land seq j (+ F) ⇝ x)) \land (m \in ℕ \land f : (1 \dots m) \underset{1-1 onto}{⟶} A)) \to A \subseteq ℝ$
16		ltso	$⊢ < Or ℝ$
17		soss	$⊢ A \subseteq ℝ \to (< Or ℝ \to < Or A)$
18	15 16 17	mpisyl	$⊢ (((φ \land j \in ℤ) \land (A \subseteq ℤ_{\geq j} \land seq j (+ F) ⇝ x)) \land (m \in ℕ \land f : (1 \dots m) \underset{1-1 onto}{⟶} A)) \to < Or A$
19		fzfi	$⊢ (1 \dots m) \in Fin$
20		ovex	$⊢ (1 \dots m) \in V$
21	20	f1oen	$⊢ f : (1 \dots m) \underset{1-1 onto}{⟶} A \to (1 \dots m) \approx A$
22	21	ad2antll	$⊢ (((φ \land j \in ℤ) \land (A \subseteq ℤ_{\geq j} \land seq j (+ F) ⇝ x)) \land (m \in ℕ \land f : (1 \dots m) \underset{1-1 onto}{⟶} A)) \to (1 \dots m) \approx A$
23	22	ensymd	$⊢ (((φ \land j \in ℤ) \land (A \subseteq ℤ_{\geq j} \land seq j (+ F) ⇝ x)) \land (m \in ℕ \land f : (1 \dots m) \underset{1-1 onto}{⟶} A)) \to A \approx (1 \dots m)$
24		enfii	$⊢ ((1 \dots m) \in Fin \land A \approx (1 \dots m)) \to A \in Fin$
25	19 23 24	sylancr	$⊢ (((φ \land j \in ℤ) \land (A \subseteq ℤ_{\geq j} \land seq j (+ F) ⇝ x)) \land (m \in ℕ \land f : (1 \dots m) \underset{1-1 onto}{⟶} A)) \to A \in Fin$
26		fz1iso	$⊢ (< Or A \land A \in Fin) \to \exists g g {Isom}_{<, <} ((1 \dots \|A\|), A)$
27	18 25 26	syl2anc	$⊢ (((φ \land j \in ℤ) \land (A \subseteq ℤ_{\geq j} \land seq j (+ F) ⇝ x)) \land (m \in ℕ \land f : (1 \dots m) \underset{1-1 onto}{⟶} A)) \to \exists g g {Isom}_{<, <} ((1 \dots \|A\|), A)$
28	2	ad5ant15	$⊢ ((((φ \land j \in ℤ) \land (A \subseteq ℤ_{\geq j} \land seq j (+ F) ⇝ x)) \land ((m \in ℕ \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land g {Isom}_{<, <} ((1 \dots \|A\|), A))) \land k \in A) \to B \in ℂ$
29		eqid	$⊢ (n \in ℕ ⟼ ⦋ g (n) / k ⦌ B) = (n \in ℕ ⟼ ⦋ g (n) / k ⦌ B)$
30		simprll	$⊢ (((φ \land j \in ℤ) \land (A \subseteq ℤ_{\geq j} \land seq j (+ F) ⇝ x)) \land ((m \in ℕ \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land g {Isom}_{<, <} ((1 \dots \|A\|), A))) \to m \in ℕ$
31		simpllr	$⊢ (((φ \land j \in ℤ) \land (A \subseteq ℤ_{\geq j} \land seq j (+ F) ⇝ x)) \land ((m \in ℕ \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land g {Isom}_{<, <} ((1 \dots \|A\|), A))) \to j \in ℤ$
32		simplrl	$⊢ (((φ \land j \in ℤ) \land (A \subseteq ℤ_{\geq j} \land seq j (+ F) ⇝ x)) \land ((m \in ℕ \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land g {Isom}_{<, <} ((1 \dots \|A\|), A))) \to A \subseteq ℤ_{\geq j}$
33		simprlr	$⊢ (((φ \land j \in ℤ) \land (A \subseteq ℤ_{\geq j} \land seq j (+ F) ⇝ x)) \land ((m \in ℕ \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land g {Isom}_{<, <} ((1 \dots \|A\|), A))) \to f : (1 \dots m) \underset{1-1 onto}{⟶} A$
34		simprr	$⊢ (((φ \land j \in ℤ) \land (A \subseteq ℤ_{\geq j} \land seq j (+ F) ⇝ x)) \land ((m \in ℕ \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land g {Isom}_{<, <} ((1 \dots \|A\|), A))) \to g {Isom}_{<, <} ((1 \dots \|A\|), A)$
35	1 28 3 29 30 31 32 33 34	summolem2a	$⊢ (((φ \land j \in ℤ) \land (A \subseteq ℤ_{\geq j} \land seq j (+ F) ⇝ x)) \land ((m \in ℕ \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land g {Isom}_{<, <} ((1 \dots \|A\|), A))) \to seq j (+ F) ⇝ seq 1 (+ G) (m)$
36	35	expr	$⊢ (((φ \land j \in ℤ) \land (A \subseteq ℤ_{\geq j} \land seq j (+ F) ⇝ x)) \land (m \in ℕ \land f : (1 \dots m) \underset{1-1 onto}{⟶} A)) \to (g {Isom}_{<, <} ((1 \dots \|A\|), A) \to seq j (+ F) ⇝ seq 1 (+ G) (m))$
37	36	exlimdv	$⊢ (((φ \land j \in ℤ) \land (A \subseteq ℤ_{\geq j} \land seq j (+ F) ⇝ x)) \land (m \in ℕ \land f : (1 \dots m) \underset{1-1 onto}{⟶} A)) \to (\exists g g {Isom}_{<, <} ((1 \dots \|A\|), A) \to seq j (+ F) ⇝ seq 1 (+ G) (m))$
38	27 37	mpd	$⊢ (((φ \land j \in ℤ) \land (A \subseteq ℤ_{\geq j} \land seq j (+ F) ⇝ x)) \land (m \in ℕ \land f : (1 \dots m) \underset{1-1 onto}{⟶} A)) \to seq j (+ F) ⇝ seq 1 (+ G) (m)$
39		climuni	$⊢ (seq j (+ F) ⇝ x \land seq j (+ F) ⇝ seq 1 (+ G) (m)) \to x = seq 1 (+ G) (m)$
40	10 38 39	syl2anc	$⊢ (((φ \land j \in ℤ) \land (A \subseteq ℤ_{\geq j} \land seq j (+ F) ⇝ x)) \land (m \in ℕ \land f : (1 \dots m) \underset{1-1 onto}{⟶} A)) \to x = seq 1 (+ G) (m)$
41	40	anassrs	$⊢ ((((φ \land j \in ℤ) \land (A \subseteq ℤ_{\geq j} \land seq j (+ F) ⇝ x)) \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \to x = seq 1 (+ G) (m)$
42		eqeq2	$⊢ y = seq 1 (+ G) (m) \to (x = y \leftrightarrow x = seq 1 (+ G) (m))$
43	41 42	syl5ibrcom	$⊢ ((((φ \land j \in ℤ) \land (A \subseteq ℤ_{\geq j} \land seq j (+ F) ⇝ x)) \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \to (y = seq 1 (+ G) (m) \to x = y)$
44	43	expimpd	$⊢ (((φ \land j \in ℤ) \land (A \subseteq ℤ_{\geq j} \land seq j (+ F) ⇝ x)) \land m \in ℕ) \to ((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ G) (m)) \to x = y)$
45	44	exlimdv	$⊢ (((φ \land j \in ℤ) \land (A \subseteq ℤ_{\geq j} \land seq j (+ F) ⇝ x)) \land m \in ℕ) \to (\exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ G) (m)) \to x = y)$
46	45	rexlimdva	$⊢ ((φ \land j \in ℤ) \land (A \subseteq ℤ_{\geq j} \land seq j (+ F) ⇝ x)) \to (\exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ G) (m)) \to x = y)$
47	46	r19.29an	$⊢ (φ \land \exists j \in ℤ (A \subseteq ℤ_{\geq j} \land seq j (+ F) ⇝ x)) \to (\exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ G) (m)) \to x = y)$
48	9 47	sylan2b	$⊢ (φ \land \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x)) \to (\exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ G) (m)) \to x = y)$

Metamath Proof Explorer

Theorem summolem2

Proof