Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem seqsuclem 4669

Description: Lemma for seqsuc 4671.

**Hypotheses**
Ref	Expression
seqval.1	⊢ S ∈ V
seqval.2	⊢ F ∈ V
seqval.3	⊢ G = (rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)
seqval.4	⊢ H = {⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(F ‘((1^st ‘z) + 1)))⟩}

**Assertion**
Ref	Expression
seqsuclem	⊢ (A ∈ ℕ → ((SseqF) ‘(A + 1)) = (((SseqF) ‘A)S(F ‘(A + 1))))

Distinct variable group(s): z,w,F z,S,w

**Proof of Theorem seqsuclem**
Step	Hyp	Ref	Expression
1		nnz 4582	. . . . . . . 8 ⊢ ℕ = {x ∈ ℤ∣1 ≤ x}
2	1	eleq2i 1153	. . . . . . 7 ⊢ (A ∈ ℕ ↔ A ∈ {x ∈ ℤ∣1 ≤ x})
3		1z 4584	. . . . . . . 8 ⊢ 1 ∈ ℤ
4		seqval.3	. . . . . . . 8 ⊢ G = (rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)
5	3, 4	uzrdgsuc 4659	. . . . . . 7 ⊢ (A ∈ {x ∈ ℤ∣1 ≤ x} → ((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘(A + 1)) = (H ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A)))
6	2, 5	sylbi 174	. . . . . 6 ⊢ (A ∈ ℕ → ((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘(A + 1)) = (H ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A)))
7		seqval.4	. . . . . . . 8 ⊢ H = {⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(F ‘((1^st ‘z) + 1)))⟩}
8		opeq12 1878	. . . . . . . . . . . 12 ⊢ ((((1^st ‘x) + 1) = ((1^st ‘z) + 1) ∧ ((2^nd ‘x)S(F ‘((1^st ‘x) + 1))) = ((2^nd ‘z)S(F ‘((1^st ‘z) + 1)))) → ⟨((1^st ‘x) + 1), ((2^nd ‘x)S(F ‘((1^st ‘x) + 1)))⟩ = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(F ‘((1^st ‘z) + 1)))⟩)
9		fveq2 2832	. . . . . . . . . . . . 13 ⊢ (x = z → (1^st ‘x) = (1^st ‘z))
10	9	opreq1d 3012	. . . . . . . . . . . 12 ⊢ (x = z → ((1^st ‘x) + 1) = ((1^st ‘z) + 1))
11		fveq2 2832	. . . . . . . . . . . . 13 ⊢ (x = z → (2^nd ‘x) = (2^nd ‘z))
12	10	fveq2d 2836	. . . . . . . . . . . . 13 ⊢ (x = z → (F ‘((1^st ‘x) + 1)) = (F ‘((1^st ‘z) + 1)))
13	11, 12	opreq12d 3014	. . . . . . . . . . . 12 ⊢ (x = z → ((2^nd ‘x)S(F ‘((1^st ‘x) + 1))) = ((2^nd ‘z)S(F ‘((1^st ‘z) + 1))))
14	8, 10, 13	sylanc 361	. . . . . . . . . . 11 ⊢ (x = z → ⟨((1^st ‘x) + 1), ((2^nd ‘x)S(F ‘((1^st ‘x) + 1)))⟩ = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(F ‘((1^st ‘z) + 1)))⟩)
15	14	cleq2d 1112	. . . . . . . . . 10 ⊢ (x = z → (y = ⟨((1^st ‘x) + 1), ((2^nd ‘x)S(F ‘((1^st ‘x) + 1)))⟩ ↔ y = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(F ‘((1^st ‘z) + 1)))⟩))
16		cleq1 1107	. . . . . . . . . 10 ⊢ (y = w → (y = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(F ‘((1^st ‘z) + 1)))⟩ ↔ w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(F ‘((1^st ‘z) + 1)))⟩))
17	15, 16	sylan9bb 418	. . . . . . . . 9 ⊢ ((x = z ∧ y = w) → (y = ⟨((1^st ‘x) + 1), ((2^nd ‘x)S(F ‘((1^st ‘x) + 1)))⟩ ↔ w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(F ‘((1^st ‘z) + 1)))⟩))
18	17	cbvopabv 2105	. . . . . . . 8 ⊢ {⟨x, y⟩∣y = ⟨((1^st ‘x) + 1), ((2^nd ‘x)S(F ‘((1^st ‘x) + 1)))⟩} = {⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(F ‘((1^st ‘z) + 1)))⟩}
19	7, 18	eqtr4 1122	. . . . . . 7 ⊢ H = {⟨x, y⟩∣y = ⟨((1^st ‘x) + 1), ((2^nd ‘x)S(F ‘((1^st ‘x) + 1)))⟩}
20		fvex 2838	. . . . . . 7 ⊢ ((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A) ∈ V
21	19, 20	seqrval 4664	. . . . . 6 ⊢ (H ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A)) = ⟨((1^st ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A)) + 1), ((2^nd ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A))S(F ‘((1^st ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A)) + 1)))⟩
22	6, 21	syl6eq 1140	. . . . 5 ⊢ (A ∈ ℕ → ((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘(A + 1)) = ⟨((1^st ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A)) + 1), ((2^nd ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A))S(F ‘((1^st ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A)) + 1)))⟩)
23	22	fveq2d 2836	. . . 4 ⊢ (A ∈ ℕ → (2^nd ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘(A + 1))) = (2^nd ‘⟨((1^st ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A)) + 1), ((2^nd ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A))S(F ‘((1^st ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A)) + 1)))⟩))
24		oprex 3018	. . . . 5 ⊢ ((1^st ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A)) + 1) ∈ V
25		oprex 3018	. . . . 5 ⊢ ((2^nd ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A))S(F ‘((1^st ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A)) + 1))) ∈ V
26	24, 25	op2nd 3092	. . . 4 ⊢ (2^nd ‘⟨((1^st ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A)) + 1), ((2^nd ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A))S(F ‘((1^st ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A)) + 1)))⟩) = ((2^nd ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A))S(F ‘((1^st ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A)) + 1)))
27	23, 26	syl6eq 1140	. . 3 ⊢ (A ∈ ℕ → (2^nd ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘(A + 1))) = ((2^nd ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A))S(F ‘((1^st ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A)) + 1))))
28	4	seqlem1 4662	. . . . . . 7 ⊢ (A ∈ ℕ → (1^st ‘((rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(F ‘((1^st ‘z) + 1)))⟩}, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A)) = A)
29		rdgeq1 2972	. . . . . . . . . . 11 ⊢ (H = {⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(F ‘((1^st ‘z) + 1)))⟩} → rec(H, ⟨1, (F ‘1)⟩) = rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(F ‘((1^st ‘z) + 1)))⟩}, ⟨1, (F ‘1)⟩))
30	7, 29	ax-mp 6	. . . . . . . . . 10 ⊢ rec(H, ⟨1, (F ‘1)⟩) = rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(F ‘((1^st ‘z) + 1)))⟩}, ⟨1, (F ‘1)⟩)
31	30	coeq1i 2504	. . . . . . . . 9 ⊢ (rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) = (rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(F ‘((1^st ‘z) + 1)))⟩}, ⟨1, (F ‘1)⟩) ∘ ^◡G)
32	31	fveq1i 2833	. . . . . . . 8 ⊢ ((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A) = ((rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(F ‘((1^st ‘z) + 1)))⟩}, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A)
33	32	fveq2i 2835	. . . . . . 7 ⊢ (1^st ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A)) = (1^st ‘((rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(F ‘((1^st ‘z) + 1)))⟩}, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A))
34	28, 33	syl5eq 1136	. . . . . 6 ⊢ (A ∈ ℕ → (1^st ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A)) = A)
35	34	opreq1d 3012	. . . . 5 ⊢ (A ∈ ℕ → ((1^st ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A)) + 1) = (A + 1))
36	35	fveq2d 2836	. . . 4 ⊢ (A ∈ ℕ → (F ‘((1^st ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A)) + 1)) = (F ‘(A + 1)))
37	36	opreq2d 3013	. . 3 ⊢ (A ∈ ℕ → ((2^nd ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A))S(F ‘((1^st ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A)) + 1))) = ((2^nd ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A))S(F ‘(A + 1))))
38	27, 37	eqtrd 1128	. 2 ⊢ (A ∈ ℕ → (2^nd ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘(A + 1))) = ((2^nd ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A))S(F ‘(A + 1))))
39		peano2nn 4433	. . 3 ⊢ (A ∈ ℕ → (A + 1) ∈ ℕ)
40		seqval.1	. . . 4 ⊢ S ∈ V
41		seqval.2	. . . 4 ⊢ F ∈ V
42	40, 41, 4, 7	seqval2 4667	. . 3 ⊢ ((A + 1) ∈ ℕ → ((SseqF) ‘(A + 1)) = (2^nd ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘(A + 1))))
43	39, 42	syl 12	. 2 ⊢ (A ∈ ℕ → ((SseqF) ‘(A + 1)) = (2^nd ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘(A + 1))))
44	40, 41, 4, 7	seqval2 4667	. . 3 ⊢ (A ∈ ℕ → ((SseqF) ‘A) = (2^nd ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A)))
45	44	opreq1d 3012	. 2 ⊢ (A ∈ ℕ → (((SseqF) ‘A)S(F ‘(A + 1))) = ((2^nd ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘A))S(F ‘(A + 1))))
46	38, 43, 45	3eqtr4d 1134	1 ⊢ (A ∈ ℕ → ((SseqF) ‘(A + 1)) = (((SseqF) ‘A)S(F ‘(A + 1))))

Colors of variables: wff set class

Syntax hints: → wi 2 = weq 797 = wceq 1091 ∈ wcel 1092 {crab 1204 Vcvv 1348 ⟨cop 1810 class class class wbr 2054 {copab 2055 ωcom 2372 ^◡ccnv 2409 ↾ cres 2412 ∘ ccom 2414 ‘cfv 2422 reccrdg 2969 (class class class)co 3001 1^st c1st 3085 2^nd c2nd 3086 1c1 4029 + caddc 4031 ≤ cle 4092 ℕcn 4093 ℤcz 4095 seqcseq 4660

This theorem is referenced by: seqsuc 4671

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077 ax-reg 1078 ax-inf 1079

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ne 1192 df-ral 1205 df-rex 1206 df-reu 1207 df-rab 1208 df-v 1349 df-sbc 1441 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-pss 1494 df-nul 1708 df-if 1777 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-int 1966 df-iun 1996 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-lim 2204 df-suc 2205 df-om 2373 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-f 2434 df-f1 2435 df-fo 2436 df-f1o 2437 df-fv 2438 df-rdg 2970 df-opr 3003 df-oprab 3004 df-1st 3087 df-2nd 3088 df-1o 3104 df-oadd 3106 df-omul 3107 df-er 3200 df-ec 3202 df-qs 3205 df-ni 3794 df-pli 3795 df-mi 3796 df-lti 3797 df-plpq 3829 df-mpq 3830 df-enq 3831 df-nq 3832 df-plq 3833 df-mq 3834 df-rq 3835 df-ltq 3836 df-1q 3837 df-np 3880 df-1p 3881 df-plp 3882 df-mp 3883 df-ltp 3884 df-plpr 3958 df-mpr 3959 df-enr 3960 df-nr 3961 df-plr 3962 df-mr 3963 df-ltr 3964 df-0r 3965 df-1r 3966 df-m1r 3967 df-c 4034 df-0 4035 df-1 4036 df-r 4038 df-plus 4039 df-mul 4040 df-lt 4041 df-sub 4133 df-neg 4135 df-le 4277 df-n 4423 df-n0 4535 df-z 4564 df-seq 4661

metamath.org