prodmo

Description: A product has at most one limit. (Contributed by Scott Fenton, 4-Dec-2017)

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

Proof

Step	Hyp	Ref	Expression
1		prodmo.1	$⊢ F = (k \in ℤ ⟼ if (k \in A, B, 1))$
2		prodmo.2	$⊢ (φ \land k \in A) \to B \in ℂ$
3		prodmo.3	$⊢ G = (j \in ℕ ⟼ ⦋ f (j) / k ⦌ B)$
4		3simpb	$⊢ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land seq m (\times F) ⇝ x) \to (A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ x)$
5	4	reximi	$⊢ \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land seq m (\times F) ⇝ x) \to \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ x)$
6		3simpb	$⊢ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land seq m (\times F) ⇝ z) \to (A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ z)$
7	6	reximi	$⊢ \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land seq m (\times F) ⇝ z) \to \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ z)$
8		fveq2	$⊢ m = w \to ℤ_{\geq m} = ℤ_{\geq w}$
9	8	sseq2d	$⊢ m = w \to (A \subseteq ℤ_{\geq m} \leftrightarrow A \subseteq ℤ_{\geq w})$
10		seqeq1	$⊢ m = w \to seq m (\times F) = seq w (\times F)$
11	10	breq1d	$⊢ m = w \to (seq m (\times F) ⇝ z \leftrightarrow seq w (\times F) ⇝ z)$
12	9 11	anbi12d	$⊢ m = w \to ((A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ z) \leftrightarrow (A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ z))$
13	12	cbvrexvw	$⊢ \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ z) \leftrightarrow \exists w \in ℤ (A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ z)$
14	13	anbi2i	$⊢ (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ x) \land \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ z)) \leftrightarrow (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ x) \land \exists w \in ℤ (A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ z))$
15		reeanv	$⊢ \exists m \in ℤ \exists w \in ℤ ((A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ x) \land (A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ z)) \leftrightarrow (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ x) \land \exists w \in ℤ (A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ z))$
16	14 15	bitr4i	$⊢ (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ x) \land \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ z)) \leftrightarrow \exists m \in ℤ \exists w \in ℤ ((A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ x) \land (A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ z))$
17		simprlr	$⊢ ((m \in ℤ \land w \in ℤ) \land ((A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ x) \land (A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ z))) \to seq m (\times F) ⇝ x$
18	17	adantl	$⊢ (φ \land ((m \in ℤ \land w \in ℤ) \land ((A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ x) \land (A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ z)))) \to seq m (\times F) ⇝ x$
19	2	adantlr	$⊢ ((φ \land ((m \in ℤ \land w \in ℤ) \land ((A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ x) \land (A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ z)))) \land k \in A) \to B \in ℂ$
20		simprll	$⊢ (φ \land ((m \in ℤ \land w \in ℤ) \land ((A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ x) \land (A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ z)))) \to m \in ℤ$
21		simprlr	$⊢ (φ \land ((m \in ℤ \land w \in ℤ) \land ((A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ x) \land (A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ z)))) \to w \in ℤ$
22		simprll	$⊢ ((m \in ℤ \land w \in ℤ) \land ((A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ x) \land (A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ z))) \to A \subseteq ℤ_{\geq m}$
23	22	adantl	$⊢ (φ \land ((m \in ℤ \land w \in ℤ) \land ((A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ x) \land (A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ z)))) \to A \subseteq ℤ_{\geq m}$
24		simprrl	$⊢ ((m \in ℤ \land w \in ℤ) \land ((A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ x) \land (A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ z))) \to A \subseteq ℤ_{\geq w}$
25	24	adantl	$⊢ (φ \land ((m \in ℤ \land w \in ℤ) \land ((A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ x) \land (A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ z)))) \to A \subseteq ℤ_{\geq w}$
26	1 19 20 21 23 25	prodrb	$⊢ (φ \land ((m \in ℤ \land w \in ℤ) \land ((A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ x) \land (A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ z)))) \to (seq m (\times F) ⇝ x \leftrightarrow seq w (\times F) ⇝ x)$
27	18 26	mpbid	$⊢ (φ \land ((m \in ℤ \land w \in ℤ) \land ((A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ x) \land (A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ z)))) \to seq w (\times F) ⇝ x$
28		simprrr	$⊢ ((m \in ℤ \land w \in ℤ) \land ((A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ x) \land (A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ z))) \to seq w (\times F) ⇝ z$
29	28	adantl	$⊢ (φ \land ((m \in ℤ \land w \in ℤ) \land ((A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ x) \land (A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ z)))) \to seq w (\times F) ⇝ z$
30		climuni	$⊢ (seq w (\times F) ⇝ x \land seq w (\times F) ⇝ z) \to x = z$
31	27 29 30	syl2anc	$⊢ (φ \land ((m \in ℤ \land w \in ℤ) \land ((A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ x) \land (A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ z)))) \to x = z$
32	31	expcom	$⊢ ((m \in ℤ \land w \in ℤ) \land ((A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ x) \land (A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ z))) \to (φ \to x = z)$
33	32	ex	$⊢ (m \in ℤ \land w \in ℤ) \to (((A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ x) \land (A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ z)) \to (φ \to x = z))$
34	33	rexlimivv	$⊢ \exists m \in ℤ \exists w \in ℤ ((A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ x) \land (A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ z)) \to (φ \to x = z)$
35	16 34	sylbi	$⊢ (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ x) \land \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ z)) \to (φ \to x = z)$
36	5 7 35	syl2an	$⊢ (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land seq m (\times F) ⇝ x) \land \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land seq m (\times F) ⇝ z)) \to (φ \to x = z)$
37	1 2 3	prodmolem2	$⊢ (φ \land \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land seq m (\times F) ⇝ z)) \to (\exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m)) \to z = x)$
38		equcomi	$⊢ z = x \to x = z$
39	37 38	syl6	$⊢ (φ \land \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land seq m (\times F) ⇝ z)) \to (\exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m)) \to x = z)$
40	39	expimpd	$⊢ φ \to ((\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land seq m (\times F) ⇝ z) \land \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m))) \to x = z)$
41	40	com12	$⊢ (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land seq m (\times F) ⇝ z) \land \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m))) \to (φ \to x = z)$
42	41	ancoms	$⊢ (\exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m)) \land \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land seq m (\times F) ⇝ z)) \to (φ \to x = z)$
43	1 2 3	prodmolem2	$⊢ (φ \land \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land seq m (\times F) ⇝ x)) \to (\exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times G) (m)) \to x = z)$
44	43	expimpd	$⊢ φ \to ((\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land seq m (\times F) ⇝ x) \land \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times G) (m))) \to x = z)$
45	44	com12	$⊢ (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land seq m (\times F) ⇝ x) \land \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times G) (m))) \to (φ \to x = z)$
46		reeanv	$⊢ \exists m \in ℕ \exists w \in ℕ (\exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m)) \land \exists g (g : (1 \dots w) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B)) (w))) \leftrightarrow (\exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m)) \land \exists w \in ℕ \exists g (g : (1 \dots w) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B)) (w)))$
47		exdistrv	$⊢ \exists f \exists g ((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m)) \land (g : (1 \dots w) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B)) (w))) \leftrightarrow (\exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m)) \land \exists g (g : (1 \dots w) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B)) (w)))$
48	47	2rexbii	$⊢ \exists m \in ℕ \exists w \in ℕ \exists f \exists g ((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m)) \land (g : (1 \dots w) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B)) (w))) \leftrightarrow \exists m \in ℕ \exists w \in ℕ (\exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m)) \land \exists g (g : (1 \dots w) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B)) (w)))$
49		oveq2	$⊢ m = w \to (1 \dots m) = (1 \dots w)$
50	49	f1oeq2d	$⊢ m = w \to (f : (1 \dots m) \underset{1-1 onto}{⟶} A \leftrightarrow f : (1 \dots w) \underset{1-1 onto}{⟶} A)$
51		fveq2	$⊢ m = w \to seq 1 (\times G) (m) = seq 1 (\times G) (w)$
52	51	eqeq2d	$⊢ m = w \to (z = seq 1 (\times G) (m) \leftrightarrow z = seq 1 (\times G) (w))$
53	50 52	anbi12d	$⊢ m = w \to ((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times G) (m)) \leftrightarrow (f : (1 \dots w) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times G) (w)))$
54	53	exbidv	$⊢ m = w \to (\exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times G) (m)) \leftrightarrow \exists f (f : (1 \dots w) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times G) (w)))$
55		f1oeq1	$⊢ f = g \to (f : (1 \dots w) \underset{1-1 onto}{⟶} A \leftrightarrow g : (1 \dots w) \underset{1-1 onto}{⟶} A)$
56		fveq1	$⊢ f = g \to f (j) = g (j)$
57	56	csbeq1d	$⊢ f = g \to ⦋ f (j) / k ⦌ B = ⦋ g (j) / k ⦌ B$
58	57	mpteq2dv	$⊢ f = g \to (j \in ℕ ⟼ ⦋ f (j) / k ⦌ B) = (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B)$
59	3 58	syl5eq	$⊢ f = g \to G = (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B)$
60	59	seqeq3d	$⊢ f = g \to seq 1 (\times G) = seq 1 (\times (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B))$
61	60	fveq1d	$⊢ f = g \to seq 1 (\times G) (w) = seq 1 (\times (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B)) (w)$
62	61	eqeq2d	$⊢ f = g \to (z = seq 1 (\times G) (w) \leftrightarrow z = seq 1 (\times (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B)) (w))$
63	55 62	anbi12d	$⊢ f = g \to ((f : (1 \dots w) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times G) (w)) \leftrightarrow (g : (1 \dots w) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B)) (w)))$
64	63	cbvexvw	$⊢ \exists f (f : (1 \dots w) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times G) (w)) \leftrightarrow \exists g (g : (1 \dots w) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B)) (w))$
65	54 64	bitrdi	$⊢ m = w \to (\exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times G) (m)) \leftrightarrow \exists g (g : (1 \dots w) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B)) (w)))$
66	65	cbvrexvw	$⊢ \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times G) (m)) \leftrightarrow \exists w \in ℕ \exists g (g : (1 \dots w) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B)) (w))$
67	66	anbi2i	$⊢ (\exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m)) \land \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times G) (m))) \leftrightarrow (\exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m)) \land \exists w \in ℕ \exists g (g : (1 \dots w) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B)) (w)))$
68	46 48 67	3bitr4i	$⊢ \exists m \in ℕ \exists w \in ℕ \exists f \exists g ((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m)) \land (g : (1 \dots w) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B)) (w))) \leftrightarrow (\exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m)) \land \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times G) (m)))$
69		an4	$⊢ ((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m)) \land (g : (1 \dots w) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B)) (w))) \leftrightarrow ((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g : (1 \dots w) \underset{1-1 onto}{⟶} A) \land (x = seq 1 (\times G) (m) \land z = seq 1 (\times (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B)) (w)))$
70	2	ad4ant14	$⊢ (((φ \land (m \in ℕ \land w \in ℕ)) \land (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g : (1 \dots w) \underset{1-1 onto}{⟶} A)) \land k \in A) \to B \in ℂ$
71		fveq2	$⊢ j = a \to f (j) = f (a)$
72	71	csbeq1d	$⊢ j = a \to ⦋ f (j) / k ⦌ B = ⦋ f (a) / k ⦌ B$
73	72	cbvmptv	$⊢ (j \in ℕ ⟼ ⦋ f (j) / k ⦌ B) = (a \in ℕ ⟼ ⦋ f (a) / k ⦌ B)$
74	3 73	eqtri	$⊢ G = (a \in ℕ ⟼ ⦋ f (a) / k ⦌ B)$
75		fveq2	$⊢ j = a \to g (j) = g (a)$
76	75	csbeq1d	$⊢ j = a \to ⦋ g (j) / k ⦌ B = ⦋ g (a) / k ⦌ B$
77	76	cbvmptv	$⊢ (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B) = (a \in ℕ ⟼ ⦋ g (a) / k ⦌ B)$
78		simplr	$⊢ ((φ \land (m \in ℕ \land w \in ℕ)) \land (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g : (1 \dots w) \underset{1-1 onto}{⟶} A)) \to (m \in ℕ \land w \in ℕ)$
79		simprl	$⊢ ((φ \land (m \in ℕ \land w \in ℕ)) \land (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g : (1 \dots w) \underset{1-1 onto}{⟶} A)) \to f : (1 \dots m) \underset{1-1 onto}{⟶} A$
80		simprr	$⊢ ((φ \land (m \in ℕ \land w \in ℕ)) \land (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g : (1 \dots w) \underset{1-1 onto}{⟶} A)) \to g : (1 \dots w) \underset{1-1 onto}{⟶} A$
81	1 70 74 77 78 79 80	prodmolem3	$⊢ ((φ \land (m \in ℕ \land w \in ℕ)) \land (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g : (1 \dots w) \underset{1-1 onto}{⟶} A)) \to seq 1 (\times G) (m) = seq 1 (\times (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B)) (w)$
82		eqeq12	$⊢ (x = seq 1 (\times G) (m) \land z = seq 1 (\times (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B)) (w)) \to (x = z \leftrightarrow seq 1 (\times G) (m) = seq 1 (\times (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B)) (w))$
83	81 82	syl5ibrcom	$⊢ ((φ \land (m \in ℕ \land w \in ℕ)) \land (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g : (1 \dots w) \underset{1-1 onto}{⟶} A)) \to ((x = seq 1 (\times G) (m) \land z = seq 1 (\times (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B)) (w)) \to x = z)$
84	83	expimpd	$⊢ (φ \land (m \in ℕ \land w \in ℕ)) \to (((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g : (1 \dots w) \underset{1-1 onto}{⟶} A) \land (x = seq 1 (\times G) (m) \land z = seq 1 (\times (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B)) (w))) \to x = z)$
85	69 84	syl5bi	$⊢ (φ \land (m \in ℕ \land w \in ℕ)) \to (((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m)) \land (g : (1 \dots w) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B)) (w))) \to x = z)$
86	85	exlimdvv	$⊢ (φ \land (m \in ℕ \land w \in ℕ)) \to (\exists f \exists g ((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m)) \land (g : (1 \dots w) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B)) (w))) \to x = z)$
87	86	rexlimdvva	$⊢ φ \to (\exists m \in ℕ \exists w \in ℕ \exists f \exists g ((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m)) \land (g : (1 \dots w) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B)) (w))) \to x = z)$
88	68 87	syl5bir	$⊢ φ \to ((\exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m)) \land \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times G) (m))) \to x = z)$
89	88	com12	$⊢ (\exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m)) \land \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times G) (m))) \to (φ \to x = z)$
90	36 42 45 89	ccase	$⊢ ((\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land seq m (\times F) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m))) \land (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land seq m (\times F) ⇝ z) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times G) (m)))) \to (φ \to x = z)$
91	90	com12	$⊢ φ \to (((\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land seq m (\times F) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m))) \land (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land seq m (\times F) ⇝ z) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times G) (m)))) \to x = z)$
92	91	alrimivv	$⊢ φ \to \forall x \forall z (((\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land seq m (\times F) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m))) \land (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land seq m (\times F) ⇝ z) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times G) (m)))) \to x = z)$
93		breq2	$⊢ x = z \to (seq m (\times F) ⇝ x \leftrightarrow seq m (\times F) ⇝ z)$
94	93	3anbi3d	$⊢ x = z \to ((A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land seq m (\times F) ⇝ x) \leftrightarrow (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land seq m (\times F) ⇝ z))$
95	94	rexbidv	$⊢ x = z \to (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land seq m (\times F) ⇝ x) \leftrightarrow \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land seq m (\times F) ⇝ z))$
96		eqeq1	$⊢ x = z \to (x = seq 1 (\times G) (m) \leftrightarrow z = seq 1 (\times G) (m))$
97	96	anbi2d	$⊢ x = z \to ((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m)) \leftrightarrow (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times G) (m)))$
98	97	exbidv	$⊢ x = z \to (\exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m)) \leftrightarrow \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times G) (m)))$
99	98	rexbidv	$⊢ x = z \to (\exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m)) \leftrightarrow \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times G) (m)))$
100	95 99	orbi12d	$⊢ x = z \to ((\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land seq m (\times F) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m))) \leftrightarrow (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land seq m (\times F) ⇝ z) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times G) (m))))$
101	100	mo4	$⊢ \exists^{*} x (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land seq m (\times F) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m))) \leftrightarrow \forall x \forall z (((\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land seq m (\times F) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m))) \land (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land seq m (\times F) ⇝ z) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times G) (m)))) \to x = z)$
102	92 101	sylibr	$⊢ φ \to \exists^{*} x (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land seq m (\times F) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times G) (m)))$

Metamath Proof Explorer

Theorem prodmo

Proof