seq1st

Description: A sequence whose iteration function ignores the second argument is only affected by the first point of the initial value function. (Contributed by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Hypotheses	algrf.1	$⊢ Z = ℤ_{\geq M}$
	algrf.2	$⊢ R = seq M ((F \circ 1^{st}), (Z \times \{A\}))$
Assertion	seq1st	$⊢ (M \in ℤ \land A \in V) \to R = seq M ((F \circ 1^{st}), \{⟨M, A⟩\})$

Proof

Step	Hyp	Ref	Expression
1		algrf.1	$⊢ Z = ℤ_{\geq M}$
2		algrf.2	$⊢ R = seq M ((F \circ 1^{st}), (Z \times \{A\}))$
3		seqfn	$⊢ M \in ℤ \to seq M ((F \circ 1^{st}), (Z \times \{A\})) Fn ℤ_{\geq M}$
4	3	adantr	$⊢ (M \in ℤ \land A \in V) \to seq M ((F \circ 1^{st}), (Z \times \{A\})) Fn ℤ_{\geq M}$
5		seqfn	$⊢ M \in ℤ \to seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) Fn ℤ_{\geq M}$
6	5	adantr	$⊢ (M \in ℤ \land A \in V) \to seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) Fn ℤ_{\geq M}$
7		fveq2	$⊢ y = M \to seq M ((F \circ 1^{st}), (Z \times \{A\})) (y) = seq M ((F \circ 1^{st}), (Z \times \{A\})) (M)$
8		fveq2	$⊢ y = M \to seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (y) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (M)$
9	7 8	eqeq12d	$⊢ y = M \to (seq M ((F \circ 1^{st}), (Z \times \{A\})) (y) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (y) \leftrightarrow seq M ((F \circ 1^{st}), (Z \times \{A\})) (M) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (M))$
10	9	imbi2d	$⊢ y = M \to ((A \in V \to seq M ((F \circ 1^{st}), (Z \times \{A\})) (y) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (y)) \leftrightarrow (A \in V \to seq M ((F \circ 1^{st}), (Z \times \{A\})) (M) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (M)))$
11		fveq2	$⊢ y = x \to seq M ((F \circ 1^{st}), (Z \times \{A\})) (y) = seq M ((F \circ 1^{st}), (Z \times \{A\})) (x)$
12		fveq2	$⊢ y = x \to seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (y) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (x)$
13	11 12	eqeq12d	$⊢ y = x \to (seq M ((F \circ 1^{st}), (Z \times \{A\})) (y) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (y) \leftrightarrow seq M ((F \circ 1^{st}), (Z \times \{A\})) (x) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (x))$
14	13	imbi2d	$⊢ y = x \to ((A \in V \to seq M ((F \circ 1^{st}), (Z \times \{A\})) (y) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (y)) \leftrightarrow (A \in V \to seq M ((F \circ 1^{st}), (Z \times \{A\})) (x) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (x)))$
15		fveq2	$⊢ y = x + 1 \to seq M ((F \circ 1^{st}), (Z \times \{A\})) (y) = seq M ((F \circ 1^{st}), (Z \times \{A\})) (x + 1)$
16		fveq2	$⊢ y = x + 1 \to seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (y) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (x + 1)$
17	15 16	eqeq12d	$⊢ y = x + 1 \to (seq M ((F \circ 1^{st}), (Z \times \{A\})) (y) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (y) \leftrightarrow seq M ((F \circ 1^{st}), (Z \times \{A\})) (x + 1) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (x + 1))$
18	17	imbi2d	$⊢ y = x + 1 \to ((A \in V \to seq M ((F \circ 1^{st}), (Z \times \{A\})) (y) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (y)) \leftrightarrow (A \in V \to seq M ((F \circ 1^{st}), (Z \times \{A\})) (x + 1) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (x + 1)))$
19		seq1	$⊢ M \in ℤ \to seq M ((F \circ 1^{st}), (Z \times \{A\})) (M) = (Z \times \{A\}) (M)$
20	19	adantr	$⊢ (M \in ℤ \land A \in V) \to seq M ((F \circ 1^{st}), (Z \times \{A\})) (M) = (Z \times \{A\}) (M)$
21		seq1	$⊢ M \in ℤ \to seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (M) = \{⟨M, A⟩\} (M)$
22	21	adantr	$⊢ (M \in ℤ \land A \in V) \to seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (M) = \{⟨M, A⟩\} (M)$
23		id	$⊢ A \in V \to A \in V$
24		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
25	24 1	eleqtrrdi	$⊢ M \in ℤ \to M \in Z$
26		fvconst2g	$⊢ (A \in V \land M \in Z) \to (Z \times \{A\}) (M) = A$
27	23 25 26	syl2anr	$⊢ (M \in ℤ \land A \in V) \to (Z \times \{A\}) (M) = A$
28		fvsng	$⊢ (M \in ℤ \land A \in V) \to \{⟨M, A⟩\} (M) = A$
29	27 28	eqtr4d	$⊢ (M \in ℤ \land A \in V) \to (Z \times \{A\}) (M) = \{⟨M, A⟩\} (M)$
30	22 29	eqtr4d	$⊢ (M \in ℤ \land A \in V) \to seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (M) = (Z \times \{A\}) (M)$
31	20 30	eqtr4d	$⊢ (M \in ℤ \land A \in V) \to seq M ((F \circ 1^{st}), (Z \times \{A\})) (M) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (M)$
32	31	ex	$⊢ M \in ℤ \to (A \in V \to seq M ((F \circ 1^{st}), (Z \times \{A\})) (M) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (M))$
33		fveq2	$⊢ seq M ((F \circ 1^{st}), (Z \times \{A\})) (x) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (x) \to F (seq M ((F \circ 1^{st}), (Z \times \{A\})) (x)) = F (seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (x))$
34		seqp1	$⊢ x \in ℤ_{\geq M} \to seq M ((F \circ 1^{st}), (Z \times \{A\})) (x + 1) = seq M ((F \circ 1^{st}), (Z \times \{A\})) (x) (F \circ 1^{st}) (Z \times \{A\}) (x + 1)$
35		fvex	$⊢ seq M ((F \circ 1^{st}), (Z \times \{A\})) (x) \in V$
36		fvex	$⊢ (Z \times \{A\}) (x + 1) \in V$
37	35 36	algrflem	$⊢ seq M ((F \circ 1^{st}), (Z \times \{A\})) (x) (F \circ 1^{st}) (Z \times \{A\}) (x + 1) = F (seq M ((F \circ 1^{st}), (Z \times \{A\})) (x))$
38	34 37	eqtrdi	$⊢ x \in ℤ_{\geq M} \to seq M ((F \circ 1^{st}), (Z \times \{A\})) (x + 1) = F (seq M ((F \circ 1^{st}), (Z \times \{A\})) (x))$
39		seqp1	$⊢ x \in ℤ_{\geq M} \to seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (x + 1) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (x) (F \circ 1^{st}) \{⟨M, A⟩\} (x + 1)$
40		fvex	$⊢ seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (x) \in V$
41		fvex	$⊢ \{⟨M, A⟩\} (x + 1) \in V$
42	40 41	algrflem	$⊢ seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (x) (F \circ 1^{st}) \{⟨M, A⟩\} (x + 1) = F (seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (x))$
43	39 42	eqtrdi	$⊢ x \in ℤ_{\geq M} \to seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (x + 1) = F (seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (x))$
44	38 43	eqeq12d	$⊢ x \in ℤ_{\geq M} \to (seq M ((F \circ 1^{st}), (Z \times \{A\})) (x + 1) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (x + 1) \leftrightarrow F (seq M ((F \circ 1^{st}), (Z \times \{A\})) (x)) = F (seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (x)))$
45	44	adantl	$⊢ (A \in V \land x \in ℤ_{\geq M}) \to (seq M ((F \circ 1^{st}), (Z \times \{A\})) (x + 1) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (x + 1) \leftrightarrow F (seq M ((F \circ 1^{st}), (Z \times \{A\})) (x)) = F (seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (x)))$
46	33 45	syl5ibr	$⊢ (A \in V \land x \in ℤ_{\geq M}) \to (seq M ((F \circ 1^{st}), (Z \times \{A\})) (x) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (x) \to seq M ((F \circ 1^{st}), (Z \times \{A\})) (x + 1) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (x + 1))$
47	46	expcom	$⊢ x \in ℤ_{\geq M} \to (A \in V \to (seq M ((F \circ 1^{st}), (Z \times \{A\})) (x) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (x) \to seq M ((F \circ 1^{st}), (Z \times \{A\})) (x + 1) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (x + 1)))$
48	47	a2d	$⊢ x \in ℤ_{\geq M} \to ((A \in V \to seq M ((F \circ 1^{st}), (Z \times \{A\})) (x) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (x)) \to (A \in V \to seq M ((F \circ 1^{st}), (Z \times \{A\})) (x + 1) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (x + 1)))$
49	10 14 18 14 32 48	uzind4	$⊢ x \in ℤ_{\geq M} \to (A \in V \to seq M ((F \circ 1^{st}), (Z \times \{A\})) (x) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (x))$
50	49	impcom	$⊢ (A \in V \land x \in ℤ_{\geq M}) \to seq M ((F \circ 1^{st}), (Z \times \{A\})) (x) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (x)$
51	50	adantll	$⊢ ((M \in ℤ \land A \in V) \land x \in ℤ_{\geq M}) \to seq M ((F \circ 1^{st}), (Z \times \{A\})) (x) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\}) (x)$
52	4 6 51	eqfnfvd	$⊢ (M \in ℤ \land A \in V) \to seq M ((F \circ 1^{st}), (Z \times \{A\})) = seq M ((F \circ 1^{st}), \{⟨M, A⟩\})$
53	2 52	syl5eq	$⊢ (M \in ℤ \land A \in V) \to R = seq M ((F \circ 1^{st}), \{⟨M, A⟩\})$

Metamath Proof Explorer

Theorem seq1st

Proof