sseqf

Description: A strong recursive sequence is a function over the nonnegative integers. (Contributed by Thierry Arnoux, 23-Apr-2019) (Proof shortened by AV, 7-Mar-2022)

	Ref	Expression
Hypotheses	sseqval.1	$⊢ φ \to S \in V$
	sseqval.2	$⊢ φ \to M \in Word S$
	sseqval.3	$⊢ W = Word S \cap {\|.\|}^{-1} [ℤ_{\geq \|M\|}]$
	sseqval.4	$⊢ φ \to F : W ⟶ S$
Assertion	sseqf	$⊢ φ \to (M {seq}_{str} F) : ℕ_{0} ⟶ S$

Proof

Step	Hyp	Ref	Expression
1		sseqval.1	$⊢ φ \to S \in V$
2		sseqval.2	$⊢ φ \to M \in Word S$
3		sseqval.3	$⊢ W = Word S \cap {\|.\|}^{-1} [ℤ_{\geq \|M\|}]$
4		sseqval.4	$⊢ φ \to F : W ⟶ S$
5		wrdf	$⊢ M \in Word S \to M : (0 ..^\|M\|) ⟶ S$
6	2 5	syl	$⊢ φ \to M : (0 ..^\|M\|) ⟶ S$
7		vex	$⊢ w \in V$
8	7	a1i	$⊢ (φ \land w \in (W ∖ \{\emptyset\})) \to w \in V$
9		fvex	$⊢ x (\|x\| - 1) \in V$
10		df-lsw	$⊢ lastS = (x \in V ⟼ x (\|x\| - 1))$
11	9 10	dmmpti	$⊢ dom lastS = V$
12	8 11	eleqtrrdi	$⊢ (φ \land w \in (W ∖ \{\emptyset\})) \to w \in dom lastS$
13		eldifsn	$⊢ w \in (W ∖ \{\emptyset\}) \leftrightarrow (w \in W \land w \neq \emptyset)$
14		inss1	$⊢ Word S \cap {\|.\|}^{-1} [ℤ_{\geq \|M\|}] \subseteq Word S$
15	3 14	eqsstri	$⊢ W \subseteq Word S$
16	15	sseli	$⊢ w \in W \to w \in Word S$
17		lswcl	$⊢ (w \in Word S \land w \neq \emptyset) \to lastS (w) \in S$
18	16 17	sylan	$⊢ (w \in W \land w \neq \emptyset) \to lastS (w) \in S$
19	13 18	sylbi	$⊢ w \in (W ∖ \{\emptyset\}) \to lastS (w) \in S$
20	19	adantl	$⊢ (φ \land w \in (W ∖ \{\emptyset\})) \to lastS (w) \in S$
21	12 20	jca	$⊢ (φ \land w \in (W ∖ \{\emptyset\})) \to (w \in dom lastS \land lastS (w) \in S)$
22	21	ralrimiva	$⊢ φ \to \forall w \in (W ∖ \{\emptyset\}) (w \in dom lastS \land lastS (w) \in S)$
23	9 10	fnmpti	$⊢ lastS Fn V$
24		fnfun	$⊢ lastS Fn V \to Fun lastS$
25		ffvresb	$⊢ Fun lastS \to (({lastS ↾}_{(W ∖ \{\emptyset\})}) : W ∖ \{\emptyset\} ⟶ S \leftrightarrow \forall w \in (W ∖ \{\emptyset\}) (w \in dom lastS \land lastS (w) \in S))$
26	23 24 25	mp2b	$⊢ ({lastS ↾}_{(W ∖ \{\emptyset\})}) : W ∖ \{\emptyset\} ⟶ S \leftrightarrow \forall w \in (W ∖ \{\emptyset\}) (w \in dom lastS \land lastS (w) \in S)$
27	22 26	sylibr	$⊢ φ \to ({lastS ↾}_{(W ∖ \{\emptyset\})}) : W ∖ \{\emptyset\} ⟶ S$
28		eqid	$⊢ ℤ_{\geq \|M\|} = ℤ_{\geq \|M\|}$
29		lencl	$⊢ M \in Word S \to \|M\| \in ℕ_{0}$
30	29	nn0zd	$⊢ M \in Word S \to \|M\| \in ℤ$
31	2 30	syl	$⊢ φ \to \|M\| \in ℤ$
32		ovex	$⊢ M ++ ⟨“ F (M) ”⟩ \in V$
33		simpr	$⊢ (φ \land a \in ℤ_{\geq \|M\|}) \to a \in ℤ_{\geq \|M\|}$
34	2 29	syl	$⊢ φ \to \|M\| \in ℕ_{0}$
35	34	adantr	$⊢ (φ \land a \in ℤ_{\geq \|M\|}) \to \|M\| \in ℕ_{0}$
36		elnn0uz	$⊢ \|M\| \in ℕ_{0} \leftrightarrow \|M\| \in ℤ_{\geq 0}$
37	35 36	sylib	$⊢ (φ \land a \in ℤ_{\geq \|M\|}) \to \|M\| \in ℤ_{\geq 0}$
38		uztrn	$⊢ (a \in ℤ_{\geq \|M\|} \land \|M\| \in ℤ_{\geq 0}) \to a \in ℤ_{\geq 0}$
39	33 37 38	syl2anc	$⊢ (φ \land a \in ℤ_{\geq \|M\|}) \to a \in ℤ_{\geq 0}$
40		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
41	39 40	eleqtrrdi	$⊢ (φ \land a \in ℤ_{\geq \|M\|}) \to a \in ℕ_{0}$
42		fvconst2g	$⊢ (M ++ ⟨“ F (M) ”⟩ \in V \land a \in ℕ_{0}) \to (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\}) (a) = M ++ ⟨“ F (M) ”⟩$
43	32 41 42	sylancr	$⊢ (φ \land a \in ℤ_{\geq \|M\|}) \to (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\}) (a) = M ++ ⟨“ F (M) ”⟩$
44	1 2 3 4	sseqmw	$⊢ φ \to M \in W$
45	4 44	ffvelrnd	$⊢ φ \to F (M) \in S$
46	45	s1cld	$⊢ φ \to ⟨“ F (M) ”⟩ \in Word S$
47		ccatcl	$⊢ (M \in Word S \land ⟨“ F (M) ”⟩ \in Word S) \to M ++ ⟨“ F (M) ”⟩ \in Word S$
48	2 46 47	syl2anc	$⊢ φ \to M ++ ⟨“ F (M) ”⟩ \in Word S$
49	32	a1i	$⊢ φ \to M ++ ⟨“ F (M) ”⟩ \in V$
50		ccatws1len	$⊢ M \in Word S \to \|M ++ ⟨“ F (M) ”⟩\| = \|M\| + 1$
51	2 50	syl	$⊢ φ \to \|M ++ ⟨“ F (M) ”⟩\| = \|M\| + 1$
52		uzid	$⊢ \|M\| \in ℤ \to \|M\| \in ℤ_{\geq \|M\|}$
53		peano2uz	$⊢ \|M\| \in ℤ_{\geq \|M\|} \to \|M\| + 1 \in ℤ_{\geq \|M\|}$
54	31 52 53	3syl	$⊢ φ \to \|M\| + 1 \in ℤ_{\geq \|M\|}$
55	51 54	eqeltrd	$⊢ φ \to \|M ++ ⟨“ F (M) ”⟩\| \in ℤ_{\geq \|M\|}$
56		hashf	$⊢ \|.\| : V ⟶ ℕ_{0} \cup \{+∞\}$
57		ffn	$⊢ \|.\| : V ⟶ ℕ_{0} \cup \{+∞\} \to \|.\| Fn V$
58		elpreima	$⊢ \|.\| Fn V \to (M ++ ⟨“ F (M) ”⟩ \in {\|.\|}^{-1} [ℤ_{\geq \|M\|}] \leftrightarrow (M ++ ⟨“ F (M) ”⟩ \in V \land \|M ++ ⟨“ F (M) ”⟩\| \in ℤ_{\geq \|M\|}))$
59	56 57 58	mp2b	$⊢ M ++ ⟨“ F (M) ”⟩ \in {\|.\|}^{-1} [ℤ_{\geq \|M\|}] \leftrightarrow (M ++ ⟨“ F (M) ”⟩ \in V \land \|M ++ ⟨“ F (M) ”⟩\| \in ℤ_{\geq \|M\|})$
60	49 55 59	sylanbrc	$⊢ φ \to M ++ ⟨“ F (M) ”⟩ \in {\|.\|}^{-1} [ℤ_{\geq \|M\|}]$
61	48 60	elind	$⊢ φ \to M ++ ⟨“ F (M) ”⟩ \in (Word S \cap {\|.\|}^{-1} [ℤ_{\geq \|M\|}])$
62	61 3	eleqtrrdi	$⊢ φ \to M ++ ⟨“ F (M) ”⟩ \in W$
63	62	adantr	$⊢ (φ \land a \in ℤ_{\geq \|M\|}) \to M ++ ⟨“ F (M) ”⟩ \in W$
64		ccatws1n0	$⊢ M \in Word S \to M ++ ⟨“ F (M) ”⟩ \neq \emptyset$
65	2 64	syl	$⊢ φ \to M ++ ⟨“ F (M) ”⟩ \neq \emptyset$
66	65	adantr	$⊢ (φ \land a \in ℤ_{\geq \|M\|}) \to M ++ ⟨“ F (M) ”⟩ \neq \emptyset$
67		eldifsn	$⊢ M ++ ⟨“ F (M) ”⟩ \in (W ∖ \{\emptyset\}) \leftrightarrow (M ++ ⟨“ F (M) ”⟩ \in W \land M ++ ⟨“ F (M) ”⟩ \neq \emptyset)$
68	63 66 67	sylanbrc	$⊢ (φ \land a \in ℤ_{\geq \|M\|}) \to M ++ ⟨“ F (M) ”⟩ \in (W ∖ \{\emptyset\})$
69	43 68	eqeltrd	$⊢ (φ \land a \in ℤ_{\geq \|M\|}) \to (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\}) (a) \in (W ∖ \{\emptyset\})$
70		eqidd	$⊢ (φ \land (a \in (W ∖ \{\emptyset\}) \land b \in (W ∖ \{\emptyset\}))) \to (x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩) = (x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩)$
71		simprl	$⊢ ((φ \land (a \in (W ∖ \{\emptyset\}) \land b \in (W ∖ \{\emptyset\}))) \land (x = a \land y = b)) \to x = a$
72	71	fveq2d	$⊢ ((φ \land (a \in (W ∖ \{\emptyset\}) \land b \in (W ∖ \{\emptyset\}))) \land (x = a \land y = b)) \to F (x) = F (a)$
73	72	s1eqd	$⊢ ((φ \land (a \in (W ∖ \{\emptyset\}) \land b \in (W ∖ \{\emptyset\}))) \land (x = a \land y = b)) \to ⟨“ F (x) ”⟩ = ⟨“ F (a) ”⟩$
74	71 73	oveq12d	$⊢ ((φ \land (a \in (W ∖ \{\emptyset\}) \land b \in (W ∖ \{\emptyset\}))) \land (x = a \land y = b)) \to x ++ ⟨“ F (x) ”⟩ = a ++ ⟨“ F (a) ”⟩$
75		vex	$⊢ a \in V$
76	75	a1i	$⊢ (φ \land (a \in (W ∖ \{\emptyset\}) \land b \in (W ∖ \{\emptyset\}))) \to a \in V$
77		vex	$⊢ b \in V$
78	77	a1i	$⊢ (φ \land (a \in (W ∖ \{\emptyset\}) \land b \in (W ∖ \{\emptyset\}))) \to b \in V$
79		ovex	$⊢ a ++ ⟨“ F (a) ”⟩ \in V$
80	79	a1i	$⊢ (φ \land (a \in (W ∖ \{\emptyset\}) \land b \in (W ∖ \{\emptyset\}))) \to a ++ ⟨“ F (a) ”⟩ \in V$
81	70 74 76 78 80	ovmpod	$⊢ (φ \land (a \in (W ∖ \{\emptyset\}) \land b \in (W ∖ \{\emptyset\}))) \to a (x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩) b = a ++ ⟨“ F (a) ”⟩$
82		eldifi	$⊢ a \in (W ∖ \{\emptyset\}) \to a \in W$
83	82	ad2antrl	$⊢ (φ \land (a \in (W ∖ \{\emptyset\}) \land b \in (W ∖ \{\emptyset\}))) \to a \in W$
84	15 83	sselid	$⊢ (φ \land (a \in (W ∖ \{\emptyset\}) \land b \in (W ∖ \{\emptyset\}))) \to a \in Word S$
85	4	adantr	$⊢ (φ \land (a \in (W ∖ \{\emptyset\}) \land b \in (W ∖ \{\emptyset\}))) \to F : W ⟶ S$
86	85 83	ffvelrnd	$⊢ (φ \land (a \in (W ∖ \{\emptyset\}) \land b \in (W ∖ \{\emptyset\}))) \to F (a) \in S$
87	86	s1cld	$⊢ (φ \land (a \in (W ∖ \{\emptyset\}) \land b \in (W ∖ \{\emptyset\}))) \to ⟨“ F (a) ”⟩ \in Word S$
88		ccatcl	$⊢ (a \in Word S \land ⟨“ F (a) ”⟩ \in Word S) \to a ++ ⟨“ F (a) ”⟩ \in Word S$
89	84 87 88	syl2anc	$⊢ (φ \land (a \in (W ∖ \{\emptyset\}) \land b \in (W ∖ \{\emptyset\}))) \to a ++ ⟨“ F (a) ”⟩ \in Word S$
90	15 82	sselid	$⊢ a \in (W ∖ \{\emptyset\}) \to a \in Word S$
91	90	ad2antrl	$⊢ (φ \land (a \in (W ∖ \{\emptyset\}) \land b \in (W ∖ \{\emptyset\}))) \to a \in Word S$
92		ccatws1len	$⊢ a \in Word S \to \|a ++ ⟨“ F (a) ”⟩\| = \|a\| + 1$
93	91 92	syl	$⊢ (φ \land (a \in (W ∖ \{\emptyset\}) \land b \in (W ∖ \{\emptyset\}))) \to \|a ++ ⟨“ F (a) ”⟩\| = \|a\| + 1$
94	83 3	eleqtrdi	$⊢ (φ \land (a \in (W ∖ \{\emptyset\}) \land b \in (W ∖ \{\emptyset\}))) \to a \in (Word S \cap {\|.\|}^{-1} [ℤ_{\geq \|M\|}])$
95	94	elin2d	$⊢ (φ \land (a \in (W ∖ \{\emptyset\}) \land b \in (W ∖ \{\emptyset\}))) \to a \in {\|.\|}^{-1} [ℤ_{\geq \|M\|}]$
96		elpreima	$⊢ \|.\| Fn V \to (a \in {\|.\|}^{-1} [ℤ_{\geq \|M\|}] \leftrightarrow (a \in V \land \|a\| \in ℤ_{\geq \|M\|}))$
97	56 57 96	mp2b	$⊢ a \in {\|.\|}^{-1} [ℤ_{\geq \|M\|}] \leftrightarrow (a \in V \land \|a\| \in ℤ_{\geq \|M\|})$
98	95 97	sylib	$⊢ (φ \land (a \in (W ∖ \{\emptyset\}) \land b \in (W ∖ \{\emptyset\}))) \to (a \in V \land \|a\| \in ℤ_{\geq \|M\|})$
99		peano2uz	$⊢ \|a\| \in ℤ_{\geq \|M\|} \to \|a\| + 1 \in ℤ_{\geq \|M\|}$
100	98 99	simpl2im	$⊢ (φ \land (a \in (W ∖ \{\emptyset\}) \land b \in (W ∖ \{\emptyset\}))) \to \|a\| + 1 \in ℤ_{\geq \|M\|}$
101	93 100	eqeltrd	$⊢ (φ \land (a \in (W ∖ \{\emptyset\}) \land b \in (W ∖ \{\emptyset\}))) \to \|a ++ ⟨“ F (a) ”⟩\| \in ℤ_{\geq \|M\|}$
102		elpreima	$⊢ \|.\| Fn V \to (a ++ ⟨“ F (a) ”⟩ \in {\|.\|}^{-1} [ℤ_{\geq \|M\|}] \leftrightarrow (a ++ ⟨“ F (a) ”⟩ \in V \land \|a ++ ⟨“ F (a) ”⟩\| \in ℤ_{\geq \|M\|}))$
103	56 57 102	mp2b	$⊢ a ++ ⟨“ F (a) ”⟩ \in {\|.\|}^{-1} [ℤ_{\geq \|M\|}] \leftrightarrow (a ++ ⟨“ F (a) ”⟩ \in V \land \|a ++ ⟨“ F (a) ”⟩\| \in ℤ_{\geq \|M\|})$
104	80 101 103	sylanbrc	$⊢ (φ \land (a \in (W ∖ \{\emptyset\}) \land b \in (W ∖ \{\emptyset\}))) \to a ++ ⟨“ F (a) ”⟩ \in {\|.\|}^{-1} [ℤ_{\geq \|M\|}]$
105	89 104	elind	$⊢ (φ \land (a \in (W ∖ \{\emptyset\}) \land b \in (W ∖ \{\emptyset\}))) \to a ++ ⟨“ F (a) ”⟩ \in (Word S \cap {\|.\|}^{-1} [ℤ_{\geq \|M\|}])$
106	105 3	eleqtrrdi	$⊢ (φ \land (a \in (W ∖ \{\emptyset\}) \land b \in (W ∖ \{\emptyset\}))) \to a ++ ⟨“ F (a) ”⟩ \in W$
107		ccatws1n0	$⊢ a \in Word S \to a ++ ⟨“ F (a) ”⟩ \neq \emptyset$
108	91 107	syl	$⊢ (φ \land (a \in (W ∖ \{\emptyset\}) \land b \in (W ∖ \{\emptyset\}))) \to a ++ ⟨“ F (a) ”⟩ \neq \emptyset$
109		eldifsn	$⊢ a ++ ⟨“ F (a) ”⟩ \in (W ∖ \{\emptyset\}) \leftrightarrow (a ++ ⟨“ F (a) ”⟩ \in W \land a ++ ⟨“ F (a) ”⟩ \neq \emptyset)$
110	106 108 109	sylanbrc	$⊢ (φ \land (a \in (W ∖ \{\emptyset\}) \land b \in (W ∖ \{\emptyset\}))) \to a ++ ⟨“ F (a) ”⟩ \in (W ∖ \{\emptyset\})$
111	81 110	eqeltrd	$⊢ (φ \land (a \in (W ∖ \{\emptyset\}) \land b \in (W ∖ \{\emptyset\}))) \to a (x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩) b \in (W ∖ \{\emptyset\})$
112	28 31 69 111	seqf	$⊢ φ \to seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})) : ℤ_{\geq \|M\|} ⟶ W ∖ \{\emptyset\}$
113		fco2	$⊢ (({lastS ↾}_{(W ∖ \{\emptyset\})}) : W ∖ \{\emptyset\} ⟶ S \land seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})) : ℤ_{\geq \|M\|} ⟶ W ∖ \{\emptyset\}) \to (lastS \circ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\}))) : ℤ_{\geq \|M\|} ⟶ S$
114	27 112 113	syl2anc	$⊢ φ \to (lastS \circ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\}))) : ℤ_{\geq \|M\|} ⟶ S$
115		fzouzdisj	$⊢ (0 ..^\|M\|) \cap ℤ_{\geq \|M\|} = \emptyset$
116	115	a1i	$⊢ φ \to (0 ..^\|M\|) \cap ℤ_{\geq \|M\|} = \emptyset$
117		fun	$⊢ ((M : (0 ..^\|M\|) ⟶ S \land (lastS \circ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\}))) : ℤ_{\geq \|M\|} ⟶ S) \land (0 ..^\|M\|) \cap ℤ_{\geq \|M\|} = \emptyset) \to (M \cup (lastS \circ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})))) : (0 ..^\|M\|) \cup ℤ_{\geq \|M\|} ⟶ S \cup S$
118	6 114 116 117	syl21anc	$⊢ φ \to (M \cup (lastS \circ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})))) : (0 ..^\|M\|) \cup ℤ_{\geq \|M\|} ⟶ S \cup S$
119	1 2 3 4	sseqval	$⊢ φ \to M {seq}_{str} F = M \cup (lastS \circ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})))$
120		fzouzsplit	$⊢ \|M\| \in ℤ_{\geq 0} \to ℤ_{\geq 0} = (0 ..^\|M\|) \cup ℤ_{\geq \|M\|}$
121	36 120	sylbi	$⊢ \|M\| \in ℕ_{0} \to ℤ_{\geq 0} = (0 ..^\|M\|) \cup ℤ_{\geq \|M\|}$
122	2 29 121	3syl	$⊢ φ \to ℤ_{\geq 0} = (0 ..^\|M\|) \cup ℤ_{\geq \|M\|}$
123	40 122	syl5eq	$⊢ φ \to ℕ_{0} = (0 ..^\|M\|) \cup ℤ_{\geq \|M\|}$
124		unidm	$⊢ S \cup S = S$
125	124	a1i	$⊢ φ \to S \cup S = S$
126	125	eqcomd	$⊢ φ \to S = S \cup S$
127	119 123 126	feq123d	$⊢ φ \to ((M {seq}_{str} F) : ℕ_{0} ⟶ S \leftrightarrow (M \cup (lastS \circ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})))) : (0 ..^\|M\|) \cup ℤ_{\geq \|M\|} ⟶ S \cup S)$
128	118 127	mpbird	$⊢ φ \to (M {seq}_{str} F) : ℕ_{0} ⟶ S$

Metamath Proof Explorer

Theorem sseqf

Proof