prodmolem2

	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	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)$

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		fveq2	$⊢ m = w \to ℤ_{\geq m} = ℤ_{\geq w}$
7	6	sseq2d	$⊢ m = w \to (A \subseteq ℤ_{\geq m} \leftrightarrow A \subseteq ℤ_{\geq w})$
8		seqeq1	$⊢ m = w \to seq m (\times F) = seq w (\times F)$
9	8	breq1d	$⊢ m = w \to (seq m (\times F) ⇝ x \leftrightarrow seq w (\times F) ⇝ x)$
10	7 9	anbi12d	$⊢ m = w \to ((A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ x) \leftrightarrow (A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ x))$
11	10	cbvrexvw	$⊢ \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (\times F) ⇝ x) \leftrightarrow \exists w \in ℤ (A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ x)$
12		reeanv	$⊢ \exists w \in ℤ \exists m \in ℕ ((A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ x) \land \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times G) (m))) \leftrightarrow (\exists w \in ℤ (A \subseteq ℤ_{\geq w} \land seq w (\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)))$
13		simprlr	$⊢ ((φ \land (w \in ℤ \land m \in ℕ)) \land ((A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ x) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A)) \to seq w (\times F) ⇝ x$
14		simprll	$⊢ ((φ \land (w \in ℤ \land m \in ℕ)) \land ((A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ x) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A)) \to A \subseteq ℤ_{\geq w}$
15		uzssz	$⊢ ℤ_{\geq w} \subseteq ℤ$
16		zssre	$⊢ ℤ \subseteq ℝ$
17	15 16	sstri	$⊢ ℤ_{\geq w} \subseteq ℝ$
18	14 17	sstrdi	$⊢ ((φ \land (w \in ℤ \land m \in ℕ)) \land ((A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ x) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A)) \to A \subseteq ℝ$
19		ltso	$⊢ < Or ℝ$
20		soss	$⊢ A \subseteq ℝ \to (< Or ℝ \to < Or A)$
21	18 19 20	mpisyl	$⊢ ((φ \land (w \in ℤ \land m \in ℕ)) \land ((A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ x) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A)) \to < Or A$
22		fzfi	$⊢ (1 \dots m) \in Fin$
23		ovex	$⊢ (1 \dots m) \in V$
24	23	f1oen	$⊢ f : (1 \dots m) \underset{1-1 onto}{⟶} A \to (1 \dots m) \approx A$
25	24	ad2antll	$⊢ ((φ \land (w \in ℤ \land m \in ℕ)) \land ((A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ x) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A)) \to (1 \dots m) \approx A$
26	25	ensymd	$⊢ ((φ \land (w \in ℤ \land m \in ℕ)) \land ((A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ x) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A)) \to A \approx (1 \dots m)$
27		enfii	$⊢ ((1 \dots m) \in Fin \land A \approx (1 \dots m)) \to A \in Fin$
28	22 26 27	sylancr	$⊢ ((φ \land (w \in ℤ \land m \in ℕ)) \land ((A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ x) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A)) \to A \in Fin$
29		fz1iso	$⊢ (< Or A \land A \in Fin) \to \exists g g {Isom}_{<, <} ((1 \dots \|A\|), A)$
30	21 28 29	syl2anc	$⊢ ((φ \land (w \in ℤ \land m \in ℕ)) \land ((A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ x) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A)) \to \exists g g {Isom}_{<, <} ((1 \dots \|A\|), A)$
31	2	ad4ant14	$⊢ (((φ \land (w \in ℤ \land m \in ℕ)) \land (((A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ x) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land g {Isom}_{<, <} ((1 \dots \|A\|), A))) \land k \in A) \to B \in ℂ$
32		eqid	$⊢ (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B) = (j \in ℕ ⟼ ⦋ g (j) / k ⦌ B)$
33		simplrr	$⊢ ((φ \land (w \in ℤ \land m \in ℕ)) \land (((A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ x) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land g {Isom}_{<, <} ((1 \dots \|A\|), A))) \to m \in ℕ$
34		simplrl	$⊢ ((φ \land (w \in ℤ \land m \in ℕ)) \land (((A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ x) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land g {Isom}_{<, <} ((1 \dots \|A\|), A))) \to w \in ℤ$
35		simplll	$⊢ (((A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ x) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land g {Isom}_{<, <} ((1 \dots \|A\|), A)) \to A \subseteq ℤ_{\geq w}$
36	35	adantl	$⊢ ((φ \land (w \in ℤ \land m \in ℕ)) \land (((A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ x) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land g {Isom}_{<, <} ((1 \dots \|A\|), A))) \to A \subseteq ℤ_{\geq w}$
37		simprlr	$⊢ ((φ \land (w \in ℤ \land m \in ℕ)) \land (((A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ x) \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$
38		simprr	$⊢ ((φ \land (w \in ℤ \land m \in ℕ)) \land (((A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ x) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land g {Isom}_{<, <} ((1 \dots \|A\|), A))) \to g {Isom}_{<, <} ((1 \dots \|A\|), A)$
39	1 31 3 32 33 34 36 37 38	prodmolem2a	$⊢ ((φ \land (w \in ℤ \land m \in ℕ)) \land (((A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ x) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land g {Isom}_{<, <} ((1 \dots \|A\|), A))) \to seq w (\times F) ⇝ seq 1 (\times G) (m)$
40	39	expr	$⊢ ((φ \land (w \in ℤ \land m \in ℕ)) \land ((A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ x) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A)) \to (g {Isom}_{<, <} ((1 \dots \|A\|), A) \to seq w (\times F) ⇝ seq 1 (\times G) (m))$
41	40	exlimdv	$⊢ ((φ \land (w \in ℤ \land m \in ℕ)) \land ((A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ x) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A)) \to (\exists g g {Isom}_{<, <} ((1 \dots \|A\|), A) \to seq w (\times F) ⇝ seq 1 (\times G) (m))$
42	30 41	mpd	$⊢ ((φ \land (w \in ℤ \land m \in ℕ)) \land ((A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ x) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A)) \to seq w (\times F) ⇝ seq 1 (\times G) (m)$
43		climuni	$⊢ (seq w (\times F) ⇝ x \land seq w (\times F) ⇝ seq 1 (\times G) (m)) \to x = seq 1 (\times G) (m)$
44	13 42 43	syl2anc	$⊢ ((φ \land (w \in ℤ \land m \in ℕ)) \land ((A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ x) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A)) \to x = seq 1 (\times G) (m)$
45		eqeq2	$⊢ z = seq 1 (\times G) (m) \to (x = z \leftrightarrow x = seq 1 (\times G) (m))$
46	44 45	syl5ibrcom	$⊢ ((φ \land (w \in ℤ \land m \in ℕ)) \land ((A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ x) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A)) \to (z = seq 1 (\times G) (m) \to x = z)$
47	46	expr	$⊢ ((φ \land (w \in ℤ \land m \in ℕ)) \land (A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ x)) \to (f : (1 \dots m) \underset{1-1 onto}{⟶} A \to (z = seq 1 (\times G) (m) \to x = z))$
48	47	impd	$⊢ ((φ \land (w \in ℤ \land m \in ℕ)) \land (A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ x)) \to ((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times G) (m)) \to x = z)$
49	48	exlimdv	$⊢ ((φ \land (w \in ℤ \land m \in ℕ)) \land (A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ x)) \to (\exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times G) (m)) \to x = z)$
50	49	expimpd	$⊢ (φ \land (w \in ℤ \land m \in ℕ)) \to (((A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ x) \land \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times G) (m))) \to x = z)$
51	50	rexlimdvva	$⊢ φ \to (\exists w \in ℤ \exists m \in ℕ ((A \subseteq ℤ_{\geq w} \land seq w (\times F) ⇝ x) \land \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land z = seq 1 (\times G) (m))) \to x = z)$
52	12 51	syl5bir	$⊢ φ \to ((\exists w \in ℤ (A \subseteq ℤ_{\geq w} \land seq w (\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)$
53	52	expdimp	$⊢ (φ \land \exists w \in ℤ (A \subseteq ℤ_{\geq w} \land seq w (\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)$
54	11 53	sylan2b	$⊢ (φ \land \exists m \in ℤ (A \subseteq ℤ_{\geq m} \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)$
55	5 54	sylan2	$⊢ (φ \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)$

Metamath Proof Explorer

Theorem prodmolem2

Proof