om2uzrdg

Description: A helper lemma for the value of a recursive definition generator on upper integers (typically either NN or NN0 ) with characteristic function F ( x , y ) and initial value A . Normally F is a function on the partition, and A is a member of the partition. See also comment in om2uz0i . (Contributed by Mario Carneiro, 26-Jun-2013) (Revised by Mario Carneiro, 18-Nov-2014)

	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⟩) ↾}_{ω}$
Assertion	om2uzrdg	$⊢ B \in ω \to R (B) = ⟨G (B), 2^{nd} (R (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		fveq2	$⊢ z = \emptyset \to R (z) = R (\emptyset)$
6		fveq2	$⊢ z = \emptyset \to G (z) = G (\emptyset)$
7		2fveq3	$⊢ z = \emptyset \to 2^{nd} (R (z)) = 2^{nd} (R (\emptyset))$
8	6 7	opeq12d	$⊢ z = \emptyset \to ⟨G (z), 2^{nd} (R (z))⟩ = ⟨G (\emptyset), 2^{nd} (R (\emptyset))⟩$
9	5 8	eqeq12d	$⊢ z = \emptyset \to (R (z) = ⟨G (z), 2^{nd} (R (z))⟩ \leftrightarrow R (\emptyset) = ⟨G (\emptyset), 2^{nd} (R (\emptyset))⟩)$
10		fveq2	$⊢ z = v \to R (z) = R (v)$
11		fveq2	$⊢ z = v \to G (z) = G (v)$
12		2fveq3	$⊢ z = v \to 2^{nd} (R (z)) = 2^{nd} (R (v))$
13	11 12	opeq12d	$⊢ z = v \to ⟨G (z), 2^{nd} (R (z))⟩ = ⟨G (v), 2^{nd} (R (v))⟩$
14	10 13	eqeq12d	$⊢ z = v \to (R (z) = ⟨G (z), 2^{nd} (R (z))⟩ \leftrightarrow R (v) = ⟨G (v), 2^{nd} (R (v))⟩)$
15		fveq2	$⊢ z = suc v \to R (z) = R (suc v)$
16		fveq2	$⊢ z = suc v \to G (z) = G (suc v)$
17		2fveq3	$⊢ z = suc v \to 2^{nd} (R (z)) = 2^{nd} (R (suc v))$
18	16 17	opeq12d	$⊢ z = suc v \to ⟨G (z), 2^{nd} (R (z))⟩ = ⟨G (suc v), 2^{nd} (R (suc v))⟩$
19	15 18	eqeq12d	$⊢ z = suc v \to (R (z) = ⟨G (z), 2^{nd} (R (z))⟩ \leftrightarrow R (suc v) = ⟨G (suc v), 2^{nd} (R (suc v))⟩)$
20		fveq2	$⊢ z = B \to R (z) = R (B)$
21		fveq2	$⊢ z = B \to G (z) = G (B)$
22		2fveq3	$⊢ z = B \to 2^{nd} (R (z)) = 2^{nd} (R (B))$
23	21 22	opeq12d	$⊢ z = B \to ⟨G (z), 2^{nd} (R (z))⟩ = ⟨G (B), 2^{nd} (R (B))⟩$
24	20 23	eqeq12d	$⊢ z = B \to (R (z) = ⟨G (z), 2^{nd} (R (z))⟩ \leftrightarrow R (B) = ⟨G (B), 2^{nd} (R (B))⟩)$
25	4	fveq1i	$⊢ R (\emptyset) = ({rec ((x \in V, y \in V ⟼ ⟨x + 1, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (\emptyset)$
26		opex	$⊢ ⟨C, A⟩ \in V$
27		fr0g	$⊢ ⟨C, A⟩ \in V \to ({rec ((x \in V, y \in V ⟼ ⟨x + 1, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (\emptyset) = ⟨C, A⟩$
28	26 27	ax-mp	$⊢ ({rec ((x \in V, y \in V ⟼ ⟨x + 1, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (\emptyset) = ⟨C, A⟩$
29	25 28	eqtri	$⊢ R (\emptyset) = ⟨C, A⟩$
30	1 2	om2uz0i	$⊢ G (\emptyset) = C$
31	29	fveq2i	$⊢ 2^{nd} (R (\emptyset)) = 2^{nd} (⟨C, A⟩)$
32	1	elexi	$⊢ C \in V$
33	32 3	op2nd	$⊢ 2^{nd} (⟨C, A⟩) = A$
34	31 33	eqtri	$⊢ 2^{nd} (R (\emptyset)) = A$
35	30 34	opeq12i	$⊢ ⟨G (\emptyset), 2^{nd} (R (\emptyset))⟩ = ⟨C, A⟩$
36	29 35	eqtr4i	$⊢ R (\emptyset) = ⟨G (\emptyset), 2^{nd} (R (\emptyset))⟩$
37		frsuc	$⊢ v \in ω \to ({rec ((x \in V, y \in V ⟼ ⟨x + 1, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (suc v) = (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⟩) ↾}_{ω}) (v))$
38	4	fveq1i	$⊢ R (suc v) = ({rec ((x \in V, y \in V ⟼ ⟨x + 1, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (suc v)$
39	4	fveq1i	$⊢ R (v) = ({rec ((x \in V, y \in V ⟼ ⟨x + 1, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (v)$
40	39	fveq2i	$⊢ (x \in V, y \in V ⟼ ⟨x + 1, x F y⟩) (R (v)) = (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⟩) ↾}_{ω}) (v))$
41	37 38 40	3eqtr4g	$⊢ v \in ω \to R (suc v) = (x \in V, y \in V ⟼ ⟨x + 1, x F y⟩) (R (v))$
42		fveq2	$⊢ R (v) = ⟨G (v), 2^{nd} (R (v))⟩ \to (x \in V, y \in V ⟼ ⟨x + 1, x F y⟩) (R (v)) = (x \in V, y \in V ⟼ ⟨x + 1, x F y⟩) (⟨G (v), 2^{nd} (R (v))⟩)$
43		df-ov	$⊢ G (v) (x \in V, y \in V ⟼ ⟨x + 1, x F y⟩) 2^{nd} (R (v)) = (x \in V, y \in V ⟼ ⟨x + 1, x F y⟩) (⟨G (v), 2^{nd} (R (v))⟩)$
44		fvex	$⊢ G (v) \in V$
45		fvex	$⊢ 2^{nd} (R (v)) \in V$
46		oveq1	$⊢ w = G (v) \to w + 1 = G (v) + 1$
47		oveq1	$⊢ w = G (v) \to w F z = G (v) F z$
48	46 47	opeq12d	$⊢ w = G (v) \to ⟨w + 1, w F z⟩ = ⟨G (v) + 1, G (v) F z⟩$
49		oveq2	$⊢ z = 2^{nd} (R (v)) \to G (v) F z = G (v) F 2^{nd} (R (v))$
50	49	opeq2d	$⊢ z = 2^{nd} (R (v)) \to ⟨G (v) + 1, G (v) F z⟩ = ⟨G (v) + 1, G (v) F 2^{nd} (R (v))⟩$
51		oveq1	$⊢ x = w \to x + 1 = w + 1$
52		oveq1	$⊢ x = w \to x F y = w F y$
53	51 52	opeq12d	$⊢ x = w \to ⟨x + 1, x F y⟩ = ⟨w + 1, w F y⟩$
54		oveq2	$⊢ y = z \to w F y = w F z$
55	54	opeq2d	$⊢ y = z \to ⟨w + 1, w F y⟩ = ⟨w + 1, w F z⟩$
56	53 55	cbvmpov	$⊢ (x \in V, y \in V ⟼ ⟨x + 1, x F y⟩) = (w \in V, z \in V ⟼ ⟨w + 1, w F z⟩)$
57		opex	$⊢ ⟨G (v) + 1, G (v) F 2^{nd} (R (v))⟩ \in V$
58	48 50 56 57	ovmpo	$⊢ (G (v) \in V \land 2^{nd} (R (v)) \in V) \to G (v) (x \in V, y \in V ⟼ ⟨x + 1, x F y⟩) 2^{nd} (R (v)) = ⟨G (v) + 1, G (v) F 2^{nd} (R (v))⟩$
59	44 45 58	mp2an	$⊢ G (v) (x \in V, y \in V ⟼ ⟨x + 1, x F y⟩) 2^{nd} (R (v)) = ⟨G (v) + 1, G (v) F 2^{nd} (R (v))⟩$
60	43 59	eqtr3i	$⊢ (x \in V, y \in V ⟼ ⟨x + 1, x F y⟩) (⟨G (v), 2^{nd} (R (v))⟩) = ⟨G (v) + 1, G (v) F 2^{nd} (R (v))⟩$
61	42 60	eqtrdi	$⊢ R (v) = ⟨G (v), 2^{nd} (R (v))⟩ \to (x \in V, y \in V ⟼ ⟨x + 1, x F y⟩) (R (v)) = ⟨G (v) + 1, G (v) F 2^{nd} (R (v))⟩$
62	41 61	sylan9eq	$⊢ (v \in ω \land R (v) = ⟨G (v), 2^{nd} (R (v))⟩) \to R (suc v) = ⟨G (v) + 1, G (v) F 2^{nd} (R (v))⟩$
63	1 2	om2uzsuci	$⊢ v \in ω \to G (suc v) = G (v) + 1$
64	63	adantr	$⊢ (v \in ω \land R (v) = ⟨G (v), 2^{nd} (R (v))⟩) \to G (suc v) = G (v) + 1$
65	62	fveq2d	$⊢ (v \in ω \land R (v) = ⟨G (v), 2^{nd} (R (v))⟩) \to 2^{nd} (R (suc v)) = 2^{nd} (⟨G (v) + 1, G (v) F 2^{nd} (R (v))⟩)$
66		ovex	$⊢ G (v) + 1 \in V$
67		ovex	$⊢ G (v) F 2^{nd} (R (v)) \in V$
68	66 67	op2nd	$⊢ 2^{nd} (⟨G (v) + 1, G (v) F 2^{nd} (R (v))⟩) = G (v) F 2^{nd} (R (v))$
69	65 68	eqtrdi	$⊢ (v \in ω \land R (v) = ⟨G (v), 2^{nd} (R (v))⟩) \to 2^{nd} (R (suc v)) = G (v) F 2^{nd} (R (v))$
70	64 69	opeq12d	$⊢ (v \in ω \land R (v) = ⟨G (v), 2^{nd} (R (v))⟩) \to ⟨G (suc v), 2^{nd} (R (suc v))⟩ = ⟨G (v) + 1, G (v) F 2^{nd} (R (v))⟩$
71	62 70	eqtr4d	$⊢ (v \in ω \land R (v) = ⟨G (v), 2^{nd} (R (v))⟩) \to R (suc v) = ⟨G (suc v), 2^{nd} (R (suc v))⟩$
72	71	ex	$⊢ v \in ω \to (R (v) = ⟨G (v), 2^{nd} (R (v))⟩ \to R (suc v) = ⟨G (suc v), 2^{nd} (R (suc v))⟩)$
73	9 14 19 24 36 72	finds	$⊢ B \in ω \to R (B) = ⟨G (B), 2^{nd} (R (B))⟩$

Metamath Proof Explorer

Theorem om2uzrdg

Proof