uzrdgsuci

Description: Successor value of a recursive definition generator on upper integers. See comment in om2uzrdg . (Contributed by Mario Carneiro, 26-Jun-2013) (Revised by Mario Carneiro, 13-Sep-2013)

	Ref	Expression
Hypotheses	om2uz.1	$⊢ C \in ℤ$
	om2uz.2	$⊢ G = {rec ((x \in V ⟼ x + 1), C) ↾}_{ω}$
	uzrdg.1	$⊢ A \in V$
	uzrdg.2	$⊢ R = {rec ((x \in V, y \in V ⟼ ⟨x + 1, x F y⟩), ⟨C, A⟩) ↾}_{ω}$
	uzrdg.3	$⊢ S = ran R$
Assertion	uzrdgsuci	$⊢ B \in ℤ_{\geq C} \to S (B + 1) = B F S (B)$

Proof

Step	Hyp	Ref	Expression
1		om2uz.1	$⊢ C \in ℤ$
2		om2uz.2	$⊢ G = {rec ((x \in V ⟼ x + 1), C) ↾}_{ω}$
3		uzrdg.1	$⊢ A \in V$
4		uzrdg.2	$⊢ R = {rec ((x \in V, y \in V ⟼ ⟨x + 1, x F y⟩), ⟨C, A⟩) ↾}_{ω}$
5		uzrdg.3	$⊢ S = ran R$
6	1 2 3 4 5	uzrdgfni	$⊢ S Fn ℤ_{\geq C}$
7		fnfun	$⊢ S Fn ℤ_{\geq C} \to Fun S$
8	6 7	ax-mp	$⊢ Fun S$
9		peano2uz	$⊢ B \in ℤ_{\geq C} \to B + 1 \in ℤ_{\geq C}$
10	1 2 3 4	uzrdglem	$⊢ B + 1 \in ℤ_{\geq C} \to ⟨B + 1, 2^{nd} (R (G^{-1} (B + 1)))⟩ \in ran R$
11	9 10	syl	$⊢ B \in ℤ_{\geq C} \to ⟨B + 1, 2^{nd} (R (G^{-1} (B + 1)))⟩ \in ran R$
12	11 5	eleqtrrdi	$⊢ B \in ℤ_{\geq C} \to ⟨B + 1, 2^{nd} (R (G^{-1} (B + 1)))⟩ \in S$
13		funopfv	$⊢ Fun S \to (⟨B + 1, 2^{nd} (R (G^{-1} (B + 1)))⟩ \in S \to S (B + 1) = 2^{nd} (R (G^{-1} (B + 1))))$
14	8 12 13	mpsyl	$⊢ B \in ℤ_{\geq C} \to S (B + 1) = 2^{nd} (R (G^{-1} (B + 1)))$
15	1 2	om2uzf1oi	$⊢ G : ω \underset{1-1 onto}{⟶} ℤ_{\geq C}$
16		f1ocnvdm	$⊢ (G : ω \underset{1-1 onto}{⟶} ℤ_{\geq C} \land B \in ℤ_{\geq C}) \to G^{-1} (B) \in ω$
17	15 16	mpan	$⊢ B \in ℤ_{\geq C} \to G^{-1} (B) \in ω$
18		peano2	$⊢ G^{-1} (B) \in ω \to suc G^{-1} (B) \in ω$
19	17 18	syl	$⊢ B \in ℤ_{\geq C} \to suc G^{-1} (B) \in ω$
20	1 2	om2uzsuci	$⊢ G^{-1} (B) \in ω \to G (suc G^{-1} (B)) = G (G^{-1} (B)) + 1$
21	17 20	syl	$⊢ B \in ℤ_{\geq C} \to G (suc G^{-1} (B)) = G (G^{-1} (B)) + 1$
22		f1ocnvfv2	$⊢ (G : ω \underset{1-1 onto}{⟶} ℤ_{\geq C} \land B \in ℤ_{\geq C}) \to G (G^{-1} (B)) = B$
23	15 22	mpan	$⊢ B \in ℤ_{\geq C} \to G (G^{-1} (B)) = B$
24	23	oveq1d	$⊢ B \in ℤ_{\geq C} \to G (G^{-1} (B)) + 1 = B + 1$
25	21 24	eqtrd	$⊢ B \in ℤ_{\geq C} \to G (suc G^{-1} (B)) = B + 1$
26		f1ocnvfv	$⊢ (G : ω \underset{1-1 onto}{⟶} ℤ_{\geq C} \land suc G^{-1} (B) \in ω) \to (G (suc G^{-1} (B)) = B + 1 \to G^{-1} (B + 1) = suc G^{-1} (B))$
27	15 26	mpan	$⊢ suc G^{-1} (B) \in ω \to (G (suc G^{-1} (B)) = B + 1 \to G^{-1} (B + 1) = suc G^{-1} (B))$
28	19 25 27	sylc	$⊢ B \in ℤ_{\geq C} \to G^{-1} (B + 1) = suc G^{-1} (B)$
29	28	fveq2d	$⊢ B \in ℤ_{\geq C} \to R (G^{-1} (B + 1)) = R (suc G^{-1} (B))$
30	29	fveq2d	$⊢ B \in ℤ_{\geq C} \to 2^{nd} (R (G^{-1} (B + 1))) = 2^{nd} (R (suc G^{-1} (B)))$
31	14 30	eqtrd	$⊢ B \in ℤ_{\geq C} \to S (B + 1) = 2^{nd} (R (suc G^{-1} (B)))$
32		frsuc	$⊢ G^{-1} (B) \in ω \to ({rec ((x \in V, y \in V ⟼ ⟨x + 1, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (suc G^{-1} (B)) = (x \in V, y \in V ⟼ ⟨x + 1, x F y⟩) (({rec ((x \in V, y \in V ⟼ ⟨x + 1, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (G^{-1} (B)))$
33	4	fveq1i	$⊢ R (suc G^{-1} (B)) = ({rec ((x \in V, y \in V ⟼ ⟨x + 1, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (suc G^{-1} (B))$
34	4	fveq1i	$⊢ R (G^{-1} (B)) = ({rec ((x \in V, y \in V ⟼ ⟨x + 1, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (G^{-1} (B))$
35	34	fveq2i	$⊢ (x \in V, y \in V ⟼ ⟨x + 1, x F y⟩) (R (G^{-1} (B))) = (x \in V, y \in V ⟼ ⟨x + 1, x F y⟩) (({rec ((x \in V, y \in V ⟼ ⟨x + 1, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (G^{-1} (B)))$
36	32 33 35	3eqtr4g	$⊢ G^{-1} (B) \in ω \to R (suc G^{-1} (B)) = (x \in V, y \in V ⟼ ⟨x + 1, x F y⟩) (R (G^{-1} (B)))$
37	1 2 3 4	om2uzrdg	$⊢ G^{-1} (B) \in ω \to R (G^{-1} (B)) = ⟨G (G^{-1} (B)), 2^{nd} (R (G^{-1} (B)))⟩$
38	37	fveq2d	$⊢ G^{-1} (B) \in ω \to (x \in V, y \in V ⟼ ⟨x + 1, x F y⟩) (R (G^{-1} (B))) = (x \in V, y \in V ⟼ ⟨x + 1, x F y⟩) (⟨G (G^{-1} (B)), 2^{nd} (R (G^{-1} (B)))⟩)$
39		df-ov	$⊢ G (G^{-1} (B)) (x \in V, y \in V ⟼ ⟨x + 1, x F y⟩) 2^{nd} (R (G^{-1} (B))) = (x \in V, y \in V ⟼ ⟨x + 1, x F y⟩) (⟨G (G^{-1} (B)), 2^{nd} (R (G^{-1} (B)))⟩)$
40	38 39	eqtr4di	$⊢ G^{-1} (B) \in ω \to (x \in V, y \in V ⟼ ⟨x + 1, x F y⟩) (R (G^{-1} (B))) = G (G^{-1} (B)) (x \in V, y \in V ⟼ ⟨x + 1, x F y⟩) 2^{nd} (R (G^{-1} (B)))$
41	36 40	eqtrd	$⊢ G^{-1} (B) \in ω \to R (suc G^{-1} (B)) = G (G^{-1} (B)) (x \in V, y \in V ⟼ ⟨x + 1, x F y⟩) 2^{nd} (R (G^{-1} (B)))$
42		fvex	$⊢ G (G^{-1} (B)) \in V$
43		fvex	$⊢ 2^{nd} (R (G^{-1} (B))) \in V$
44		oveq1	$⊢ z = G (G^{-1} (B)) \to z + 1 = G (G^{-1} (B)) + 1$
45		oveq1	$⊢ z = G (G^{-1} (B)) \to z F w = G (G^{-1} (B)) F w$
46	44 45	opeq12d	$⊢ z = G (G^{-1} (B)) \to ⟨z + 1, z F w⟩ = ⟨G (G^{-1} (B)) + 1, G (G^{-1} (B)) F w⟩$
47		oveq2	$⊢ w = 2^{nd} (R (G^{-1} (B))) \to G (G^{-1} (B)) F w = G (G^{-1} (B)) F 2^{nd} (R (G^{-1} (B)))$
48	47	opeq2d	$⊢ w = 2^{nd} (R (G^{-1} (B))) \to ⟨G (G^{-1} (B)) + 1, G (G^{-1} (B)) F w⟩ = ⟨G (G^{-1} (B)) + 1, G (G^{-1} (B)) F 2^{nd} (R (G^{-1} (B)))⟩$
49		oveq1	$⊢ x = z \to x + 1 = z + 1$
50		oveq1	$⊢ x = z \to x F y = z F y$
51	49 50	opeq12d	$⊢ x = z \to ⟨x + 1, x F y⟩ = ⟨z + 1, z F y⟩$
52		oveq2	$⊢ y = w \to z F y = z F w$
53	52	opeq2d	$⊢ y = w \to ⟨z + 1, z F y⟩ = ⟨z + 1, z F w⟩$
54	51 53	cbvmpov	$⊢ (x \in V, y \in V ⟼ ⟨x + 1, x F y⟩) = (z \in V, w \in V ⟼ ⟨z + 1, z F w⟩)$
55		opex	$⊢ ⟨G (G^{-1} (B)) + 1, G (G^{-1} (B)) F 2^{nd} (R (G^{-1} (B)))⟩ \in V$
56	46 48 54 55	ovmpo	$⊢ (G (G^{-1} (B)) \in V \land 2^{nd} (R (G^{-1} (B))) \in V) \to G (G^{-1} (B)) (x \in V, y \in V ⟼ ⟨x + 1, x F y⟩) 2^{nd} (R (G^{-1} (B))) = ⟨G (G^{-1} (B)) + 1, G (G^{-1} (B)) F 2^{nd} (R (G^{-1} (B)))⟩$
57	42 43 56	mp2an	$⊢ G (G^{-1} (B)) (x \in V, y \in V ⟼ ⟨x + 1, x F y⟩) 2^{nd} (R (G^{-1} (B))) = ⟨G (G^{-1} (B)) + 1, G (G^{-1} (B)) F 2^{nd} (R (G^{-1} (B)))⟩$
58	41 57	eqtrdi	$⊢ G^{-1} (B) \in ω \to R (suc G^{-1} (B)) = ⟨G (G^{-1} (B)) + 1, G (G^{-1} (B)) F 2^{nd} (R (G^{-1} (B)))⟩$
59	58	fveq2d	$⊢ G^{-1} (B) \in ω \to 2^{nd} (R (suc G^{-1} (B))) = 2^{nd} (⟨G (G^{-1} (B)) + 1, G (G^{-1} (B)) F 2^{nd} (R (G^{-1} (B)))⟩)$
60		ovex	$⊢ G (G^{-1} (B)) + 1 \in V$
61		ovex	$⊢ G (G^{-1} (B)) F 2^{nd} (R (G^{-1} (B))) \in V$
62	60 61	op2nd	$⊢ 2^{nd} (⟨G (G^{-1} (B)) + 1, G (G^{-1} (B)) F 2^{nd} (R (G^{-1} (B)))⟩) = G (G^{-1} (B)) F 2^{nd} (R (G^{-1} (B)))$
63	59 62	eqtrdi	$⊢ G^{-1} (B) \in ω \to 2^{nd} (R (suc G^{-1} (B))) = G (G^{-1} (B)) F 2^{nd} (R (G^{-1} (B)))$
64	17 63	syl	$⊢ B \in ℤ_{\geq C} \to 2^{nd} (R (suc G^{-1} (B))) = G (G^{-1} (B)) F 2^{nd} (R (G^{-1} (B)))$
65	1 2 3 4	uzrdglem	$⊢ B \in ℤ_{\geq C} \to ⟨B, 2^{nd} (R (G^{-1} (B)))⟩ \in ran R$
66	65 5	eleqtrrdi	$⊢ B \in ℤ_{\geq C} \to ⟨B, 2^{nd} (R (G^{-1} (B)))⟩ \in S$
67		funopfv	$⊢ Fun S \to (⟨B, 2^{nd} (R (G^{-1} (B)))⟩ \in S \to S (B) = 2^{nd} (R (G^{-1} (B))))$
68	8 66 67	mpsyl	$⊢ B \in ℤ_{\geq C} \to S (B) = 2^{nd} (R (G^{-1} (B)))$
69	68	eqcomd	$⊢ B \in ℤ_{\geq C} \to 2^{nd} (R (G^{-1} (B))) = S (B)$
70	23 69	oveq12d	$⊢ B \in ℤ_{\geq C} \to G (G^{-1} (B)) F 2^{nd} (R (G^{-1} (B))) = B F S (B)$
71	31 64 70	3eqtrd	$⊢ B \in ℤ_{\geq C} \to S (B + 1) = B F S (B)$

Metamath Proof Explorer

Theorem uzrdgsuci

Proof