summo

Description: A sum has at most one limit. (Contributed by Mario Carneiro, 3-Apr-2014) (Revised by Mario Carneiro, 23-Aug-2014)

	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	summo	$⊢ φ \to \exists^{*} x (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ G) (m)))$

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 = n \to ℤ_{\geq m} = ℤ_{\geq n}$
5	4	sseq2d	$⊢ m = n \to (A \subseteq ℤ_{\geq m} \leftrightarrow A \subseteq ℤ_{\geq n})$
6		seqeq1	$⊢ m = n \to seq m (+ F) = seq n (+ F)$
7	6	breq1d	$⊢ m = n \to (seq m (+ F) ⇝ y \leftrightarrow seq n (+ F) ⇝ y)$
8	5 7	anbi12d	$⊢ m = n \to ((A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ y) \leftrightarrow (A \subseteq ℤ_{\geq n} \land seq n (+ F) ⇝ y))$
9	8	cbvrexvw	$⊢ \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ y) \leftrightarrow \exists n \in ℤ (A \subseteq ℤ_{\geq n} \land seq n (+ F) ⇝ y)$
10		reeanv	$⊢ \exists m \in ℤ \exists n \in ℤ ((A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x) \land (A \subseteq ℤ_{\geq n} \land seq n (+ F) ⇝ y)) \leftrightarrow (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x) \land \exists n \in ℤ (A \subseteq ℤ_{\geq n} \land seq n (+ F) ⇝ y))$
11		simprlr	$⊢ ((φ \land (m \in ℤ \land n \in ℤ)) \land ((A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x) \land (A \subseteq ℤ_{\geq n} \land seq n (+ F) ⇝ y))) \to seq m (+ F) ⇝ x$
12	2	ad4ant14	$⊢ (((φ \land (m \in ℤ \land n \in ℤ)) \land ((A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x) \land (A \subseteq ℤ_{\geq n} \land seq n (+ F) ⇝ y))) \land k \in A) \to B \in ℂ$
13		simplrl	$⊢ ((φ \land (m \in ℤ \land n \in ℤ)) \land ((A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x) \land (A \subseteq ℤ_{\geq n} \land seq n (+ F) ⇝ y))) \to m \in ℤ$
14		simplrr	$⊢ ((φ \land (m \in ℤ \land n \in ℤ)) \land ((A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x) \land (A \subseteq ℤ_{\geq n} \land seq n (+ F) ⇝ y))) \to n \in ℤ$
15		simprll	$⊢ ((φ \land (m \in ℤ \land n \in ℤ)) \land ((A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x) \land (A \subseteq ℤ_{\geq n} \land seq n (+ F) ⇝ y))) \to A \subseteq ℤ_{\geq m}$
16		simprrl	$⊢ ((φ \land (m \in ℤ \land n \in ℤ)) \land ((A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x) \land (A \subseteq ℤ_{\geq n} \land seq n (+ F) ⇝ y))) \to A \subseteq ℤ_{\geq n}$
17	1 12 13 14 15 16	sumrb	$⊢ ((φ \land (m \in ℤ \land n \in ℤ)) \land ((A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x) \land (A \subseteq ℤ_{\geq n} \land seq n (+ F) ⇝ y))) \to (seq m (+ F) ⇝ x \leftrightarrow seq n (+ F) ⇝ x)$
18	11 17	mpbid	$⊢ ((φ \land (m \in ℤ \land n \in ℤ)) \land ((A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x) \land (A \subseteq ℤ_{\geq n} \land seq n (+ F) ⇝ y))) \to seq n (+ F) ⇝ x$
19		simprrr	$⊢ ((φ \land (m \in ℤ \land n \in ℤ)) \land ((A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x) \land (A \subseteq ℤ_{\geq n} \land seq n (+ F) ⇝ y))) \to seq n (+ F) ⇝ y$
20		climuni	$⊢ (seq n (+ F) ⇝ x \land seq n (+ F) ⇝ y) \to x = y$
21	18 19 20	syl2anc	$⊢ ((φ \land (m \in ℤ \land n \in ℤ)) \land ((A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x) \land (A \subseteq ℤ_{\geq n} \land seq n (+ F) ⇝ y))) \to x = y$
22	21	exp31	$⊢ φ \to ((m \in ℤ \land n \in ℤ) \to (((A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x) \land (A \subseteq ℤ_{\geq n} \land seq n (+ F) ⇝ y)) \to x = y))$
23	22	rexlimdvv	$⊢ φ \to (\exists m \in ℤ \exists n \in ℤ ((A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x) \land (A \subseteq ℤ_{\geq n} \land seq n (+ F) ⇝ y)) \to x = y)$
24	10 23	syl5bir	$⊢ φ \to ((\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x) \land \exists n \in ℤ (A \subseteq ℤ_{\geq n} \land seq n (+ F) ⇝ y)) \to x = y)$
25	24	expdimp	$⊢ (φ \land \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x)) \to (\exists n \in ℤ (A \subseteq ℤ_{\geq n} \land seq n (+ F) ⇝ y) \to x = y)$
26	9 25	syl5bi	$⊢ (φ \land \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x)) \to (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ y) \to x = y)$
27	1 2 3	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)$
28	26 27	jaod	$⊢ (φ \land \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x)) \to ((\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ y) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ G) (m))) \to x = y)$
29	1 2 3	summolem2	$⊢ (φ \land \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ y)) \to (\exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ G) (m)) \to y = x)$
30		equcom	$⊢ y = x \leftrightarrow x = y$
31	29 30	syl6ib	$⊢ (φ \land \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ y)) \to (\exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ G) (m)) \to x = y)$
32	31	impancom	$⊢ (φ \land \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ G) (m))) \to (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ y) \to x = y)$
33		oveq2	$⊢ m = n \to (1 \dots m) = (1 \dots n)$
34	33	f1oeq2d	$⊢ m = n \to (f : (1 \dots m) \underset{1-1 onto}{⟶} A \leftrightarrow f : (1 \dots n) \underset{1-1 onto}{⟶} A)$
35		fveq2	$⊢ m = n \to seq 1 (+ G) (m) = seq 1 (+ G) (n)$
36	35	eqeq2d	$⊢ m = n \to (y = seq 1 (+ G) (m) \leftrightarrow y = seq 1 (+ G) (n))$
37	34 36	anbi12d	$⊢ m = n \to ((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ G) (m)) \leftrightarrow (f : (1 \dots n) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ G) (n)))$
38	37	exbidv	$⊢ m = n \to (\exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ G) (m)) \leftrightarrow \exists f (f : (1 \dots n) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ G) (n)))$
39		f1oeq1	$⊢ f = g \to (f : (1 \dots n) \underset{1-1 onto}{⟶} A \leftrightarrow g : (1 \dots n) \underset{1-1 onto}{⟶} A)$
40		fveq1	$⊢ f = g \to f (n) = g (n)$
41	40	csbeq1d	$⊢ f = g \to ⦋ f (n) / k ⦌ B = ⦋ g (n) / k ⦌ B$
42	41	mpteq2dv	$⊢ f = g \to (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B) = (n \in ℕ ⟼ ⦋ g (n) / k ⦌ B)$
43	3 42	eqtrid	$⊢ f = g \to G = (n \in ℕ ⟼ ⦋ g (n) / k ⦌ B)$
44	43	seqeq3d	$⊢ f = g \to seq 1 (+ G) = seq 1 (+ (n \in ℕ ⟼ ⦋ g (n) / k ⦌ B))$
45	44	fveq1d	$⊢ f = g \to seq 1 (+ G) (n) = seq 1 (+ (n \in ℕ ⟼ ⦋ g (n) / k ⦌ B)) (n)$
46	45	eqeq2d	$⊢ f = g \to (y = seq 1 (+ G) (n) \leftrightarrow y = seq 1 (+ (n \in ℕ ⟼ ⦋ g (n) / k ⦌ B)) (n))$
47	39 46	anbi12d	$⊢ f = g \to ((f : (1 \dots n) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ G) (n)) \leftrightarrow (g : (1 \dots n) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ (n \in ℕ ⟼ ⦋ g (n) / k ⦌ B)) (n)))$
48	47	cbvexvw	$⊢ \exists f (f : (1 \dots n) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ G) (n)) \leftrightarrow \exists g (g : (1 \dots n) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ (n \in ℕ ⟼ ⦋ g (n) / k ⦌ B)) (n))$
49	38 48	bitrdi	$⊢ m = n \to (\exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ G) (m)) \leftrightarrow \exists g (g : (1 \dots n) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ (n \in ℕ ⟼ ⦋ g (n) / k ⦌ B)) (n)))$
50	49	cbvrexvw	$⊢ \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ G) (m)) \leftrightarrow \exists n \in ℕ \exists g (g : (1 \dots n) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ (n \in ℕ ⟼ ⦋ g (n) / k ⦌ B)) (n))$
51		reeanv	$⊢ \exists m \in ℕ \exists n \in ℕ (\exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ G) (m)) \land \exists g (g : (1 \dots n) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ (n \in ℕ ⟼ ⦋ g (n) / k ⦌ B)) (n))) \leftrightarrow (\exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ G) (m)) \land \exists n \in ℕ \exists g (g : (1 \dots n) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ (n \in ℕ ⟼ ⦋ g (n) / k ⦌ B)) (n)))$
52		exdistrv	$⊢ \exists f \exists g ((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ G) (m)) \land (g : (1 \dots n) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ (n \in ℕ ⟼ ⦋ g (n) / k ⦌ B)) (n))) \leftrightarrow (\exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ G) (m)) \land \exists g (g : (1 \dots n) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ (n \in ℕ ⟼ ⦋ g (n) / k ⦌ B)) (n)))$
53		an4	$⊢ ((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ G) (m)) \land (g : (1 \dots n) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ (n \in ℕ ⟼ ⦋ g (n) / k ⦌ B)) (n))) \leftrightarrow ((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g : (1 \dots n) \underset{1-1 onto}{⟶} A) \land (x = seq 1 (+ G) (m) \land y = seq 1 (+ (n \in ℕ ⟼ ⦋ g (n) / k ⦌ B)) (n)))$
54	2	ad4ant14	$⊢ (((φ \land (m \in ℕ \land n \in ℕ)) \land (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g : (1 \dots n) \underset{1-1 onto}{⟶} A)) \land k \in A) \to B \in ℂ$
55		fveq2	$⊢ n = j \to f (n) = f (j)$
56	55	csbeq1d	$⊢ n = j \to ⦋ f (n) / k ⦌ B = ⦋ f (j) / k ⦌ B$
57	56	cbvmptv	$⊢ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B) = (j \in ℕ ⟼ ⦋ f (j) / k ⦌ B)$
58	3 57	eqtri	$⊢ G = (j \in ℕ ⟼ ⦋ f (j) / k ⦌ B)$
59		fveq2	$⊢ n = j \to g (n) = g (j)$
60	59	csbeq1d	$⊢ n = j \to ⦋ g (n) / k ⦌ B = ⦋ g (j) / k ⦌ B$
61	60	cbvmptv	$⊢ (n \in ℕ ⟼ ⦋ g (n) / k ⦌ B) = (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B)$
62		simplr	$⊢ ((φ \land (m \in ℕ \land n \in ℕ)) \land (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g : (1 \dots n) \underset{1-1 onto}{⟶} A)) \to (m \in ℕ \land n \in ℕ)$
63		simprl	$⊢ ((φ \land (m \in ℕ \land n \in ℕ)) \land (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g : (1 \dots n) \underset{1-1 onto}{⟶} A)) \to f : (1 \dots m) \underset{1-1 onto}{⟶} A$
64		simprr	$⊢ ((φ \land (m \in ℕ \land n \in ℕ)) \land (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g : (1 \dots n) \underset{1-1 onto}{⟶} A)) \to g : (1 \dots n) \underset{1-1 onto}{⟶} A$
65	1 54 58 61 62 63 64	summolem3	$⊢ ((φ \land (m \in ℕ \land n \in ℕ)) \land (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g : (1 \dots n) \underset{1-1 onto}{⟶} A)) \to seq 1 (+ G) (m) = seq 1 (+ (n \in ℕ ⟼ ⦋ g (n) / k ⦌ B)) (n)$
66		eqeq12	$⊢ (x = seq 1 (+ G) (m) \land y = seq 1 (+ (n \in ℕ ⟼ ⦋ g (n) / k ⦌ B)) (n)) \to (x = y \leftrightarrow seq 1 (+ G) (m) = seq 1 (+ (n \in ℕ ⟼ ⦋ g (n) / k ⦌ B)) (n))$
67	65 66	syl5ibrcom	$⊢ ((φ \land (m \in ℕ \land n \in ℕ)) \land (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g : (1 \dots n) \underset{1-1 onto}{⟶} A)) \to ((x = seq 1 (+ G) (m) \land y = seq 1 (+ (n \in ℕ ⟼ ⦋ g (n) / k ⦌ B)) (n)) \to x = y)$
68	67	expimpd	$⊢ (φ \land (m \in ℕ \land n \in ℕ)) \to (((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g : (1 \dots n) \underset{1-1 onto}{⟶} A) \land (x = seq 1 (+ G) (m) \land y = seq 1 (+ (n \in ℕ ⟼ ⦋ g (n) / k ⦌ B)) (n))) \to x = y)$
69	53 68	syl5bi	$⊢ (φ \land (m \in ℕ \land n \in ℕ)) \to (((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ G) (m)) \land (g : (1 \dots n) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ (n \in ℕ ⟼ ⦋ g (n) / k ⦌ B)) (n))) \to x = y)$
70	69	exlimdvv	$⊢ (φ \land (m \in ℕ \land n \in ℕ)) \to (\exists f \exists g ((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ G) (m)) \land (g : (1 \dots n) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ (n \in ℕ ⟼ ⦋ g (n) / k ⦌ B)) (n))) \to x = y)$
71	52 70	syl5bir	$⊢ (φ \land (m \in ℕ \land n \in ℕ)) \to ((\exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ G) (m)) \land \exists g (g : (1 \dots n) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ (n \in ℕ ⟼ ⦋ g (n) / k ⦌ B)) (n))) \to x = y)$
72	71	rexlimdvva	$⊢ φ \to (\exists m \in ℕ \exists n \in ℕ (\exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ G) (m)) \land \exists g (g : (1 \dots n) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ (n \in ℕ ⟼ ⦋ g (n) / k ⦌ B)) (n))) \to x = y)$
73	51 72	syl5bir	$⊢ φ \to ((\exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ G) (m)) \land \exists n \in ℕ \exists g (g : (1 \dots n) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ (n \in ℕ ⟼ ⦋ g (n) / k ⦌ B)) (n))) \to x = y)$
74	73	expdimp	$⊢ (φ \land \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ G) (m))) \to (\exists n \in ℕ \exists g (g : (1 \dots n) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ (n \in ℕ ⟼ ⦋ g (n) / k ⦌ B)) (n)) \to x = y)$
75	50 74	syl5bi	$⊢ (φ \land \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ G) (m))) \to (\exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ G) (m)) \to x = y)$
76	32 75	jaod	$⊢ (φ \land \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ G) (m))) \to ((\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ y) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ G) (m))) \to x = y)$
77	28 76	jaodan	$⊢ (φ \land (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ G) (m)))) \to ((\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ y) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ G) (m))) \to x = y)$
78	77	expimpd	$⊢ φ \to (((\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ G) (m))) \land (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ y) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ G) (m)))) \to x = y)$
79	78	alrimivv	$⊢ φ \to \forall x \forall y (((\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ G) (m))) \land (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ y) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ G) (m)))) \to x = y)$
80		breq2	$⊢ x = y \to (seq m (+ F) ⇝ x \leftrightarrow seq m (+ F) ⇝ y)$
81	80	anbi2d	$⊢ x = y \to ((A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x) \leftrightarrow (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ y))$
82	81	rexbidv	$⊢ x = y \to (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x) \leftrightarrow \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ y))$
83		eqeq1	$⊢ x = y \to (x = seq 1 (+ G) (m) \leftrightarrow y = seq 1 (+ G) (m))$
84	83	anbi2d	$⊢ x = y \to ((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ G) (m)) \leftrightarrow (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ G) (m)))$
85	84	exbidv	$⊢ x = y \to (\exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ G) (m)) \leftrightarrow \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ G) (m)))$
86	85	rexbidv	$⊢ x = y \to (\exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ G) (m)) \leftrightarrow \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ G) (m)))$
87	82 86	orbi12d	$⊢ x = y \to ((\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ G) (m))) \leftrightarrow (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ y) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ G) (m))))$
88	87	mo4	$⊢ \exists^{*} x (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ G) (m))) \leftrightarrow \forall x \forall y (((\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ G) (m))) \land (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ y) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land y = seq 1 (+ G) (m)))) \to x = y)$
89	79 88	sylibr	$⊢ φ \to \exists^{*} x (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ F) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ G) (m)))$

Metamath Proof Explorer

Theorem summo

Proof