seqomlem1

Description: Lemma for seqom . The underlying recursion generates a sequence of pairs with the expected first values. (Contributed by Stefan O'Rear, 1-Nov-2014) (Revised by Mario Carneiro, 23-Jun-2015)

		Ref	Expression
	Hypothesis	seqomlem.a	$⊢ Q = rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩)$
	Assertion	seqomlem1	$⊢ A \in ω \to Q (A) = ⟨A, 2^{nd} (Q (A))⟩$

Proof

Step	Hyp	Ref	Expression
1		seqomlem.a	$⊢ Q = rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩)$
2		fveq2	$⊢ a = \emptyset \to Q (a) = Q (\emptyset)$
3		id	$⊢ a = \emptyset \to a = \emptyset$
4		2fveq3	$⊢ a = \emptyset \to 2^{nd} (Q (a)) = 2^{nd} (Q (\emptyset))$
5	3 4	opeq12d	$⊢ a = \emptyset \to ⟨a, 2^{nd} (Q (a))⟩ = ⟨\emptyset, 2^{nd} (Q (\emptyset))⟩$
6	2 5	eqeq12d	$⊢ a = \emptyset \to (Q (a) = ⟨a, 2^{nd} (Q (a))⟩ \leftrightarrow Q (\emptyset) = ⟨\emptyset, 2^{nd} (Q (\emptyset))⟩)$
7		fveq2	$⊢ a = b \to Q (a) = Q (b)$
8		id	$⊢ a = b \to a = b$
9		2fveq3	$⊢ a = b \to 2^{nd} (Q (a)) = 2^{nd} (Q (b))$
10	8 9	opeq12d	$⊢ a = b \to ⟨a, 2^{nd} (Q (a))⟩ = ⟨b, 2^{nd} (Q (b))⟩$
11	7 10	eqeq12d	$⊢ a = b \to (Q (a) = ⟨a, 2^{nd} (Q (a))⟩ \leftrightarrow Q (b) = ⟨b, 2^{nd} (Q (b))⟩)$
12		fveq2	$⊢ a = suc b \to Q (a) = Q (suc b)$
13		id	$⊢ a = suc b \to a = suc b$
14		2fveq3	$⊢ a = suc b \to 2^{nd} (Q (a)) = 2^{nd} (Q (suc b))$
15	13 14	opeq12d	$⊢ a = suc b \to ⟨a, 2^{nd} (Q (a))⟩ = ⟨suc b, 2^{nd} (Q (suc b))⟩$
16	12 15	eqeq12d	$⊢ a = suc b \to (Q (a) = ⟨a, 2^{nd} (Q (a))⟩ \leftrightarrow Q (suc b) = ⟨suc b, 2^{nd} (Q (suc b))⟩)$
17		fveq2	$⊢ a = A \to Q (a) = Q (A)$
18		id	$⊢ a = A \to a = A$
19		2fveq3	$⊢ a = A \to 2^{nd} (Q (a)) = 2^{nd} (Q (A))$
20	18 19	opeq12d	$⊢ a = A \to ⟨a, 2^{nd} (Q (a))⟩ = ⟨A, 2^{nd} (Q (A))⟩$
21	17 20	eqeq12d	$⊢ a = A \to (Q (a) = ⟨a, 2^{nd} (Q (a))⟩ \leftrightarrow Q (A) = ⟨A, 2^{nd} (Q (A))⟩)$
22	1	fveq1i	$⊢ Q (\emptyset) = rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) (\emptyset)$
23		opex	$⊢ ⟨\emptyset, I (I)⟩ \in V$
24	23	rdg0	$⊢ rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) (\emptyset) = ⟨\emptyset, I (I)⟩$
25	22 24	eqtri	$⊢ Q (\emptyset) = ⟨\emptyset, I (I)⟩$
26		0ex	$⊢ \emptyset \in V$
27		fvex	$⊢ I (I) \in V$
28	26 27	op2nd	$⊢ 2^{nd} (⟨\emptyset, I (I)⟩) = I (I)$
29	28	eqcomi	$⊢ I (I) = 2^{nd} (⟨\emptyset, I (I)⟩)$
30	29	opeq2i	$⊢ ⟨\emptyset, I (I)⟩ = ⟨\emptyset, 2^{nd} (⟨\emptyset, I (I)⟩)⟩$
31		id	$⊢ Q (\emptyset) = ⟨\emptyset, I (I)⟩ \to Q (\emptyset) = ⟨\emptyset, I (I)⟩$
32		fveq2	$⊢ Q (\emptyset) = ⟨\emptyset, I (I)⟩ \to 2^{nd} (Q (\emptyset)) = 2^{nd} (⟨\emptyset, I (I)⟩)$
33	32	opeq2d	$⊢ Q (\emptyset) = ⟨\emptyset, I (I)⟩ \to ⟨\emptyset, 2^{nd} (Q (\emptyset))⟩ = ⟨\emptyset, 2^{nd} (⟨\emptyset, I (I)⟩)⟩$
34	30 31 33	3eqtr4a	$⊢ Q (\emptyset) = ⟨\emptyset, I (I)⟩ \to Q (\emptyset) = ⟨\emptyset, 2^{nd} (Q (\emptyset))⟩$
35	25 34	ax-mp	$⊢ Q (\emptyset) = ⟨\emptyset, 2^{nd} (Q (\emptyset))⟩$
36		df-ov	$⊢ b (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) 2^{nd} (Q (b)) = (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (⟨b, 2^{nd} (Q (b))⟩)$
37		fvex	$⊢ 2^{nd} (Q (b)) \in V$
38		suceq	$⊢ i = b \to suc i = suc b$
39		oveq1	$⊢ i = b \to i F v = b F v$
40	38 39	opeq12d	$⊢ i = b \to ⟨suc i, i F v⟩ = ⟨suc b, b F v⟩$
41		oveq2	$⊢ v = 2^{nd} (Q (b)) \to b F v = b F 2^{nd} (Q (b))$
42	41	opeq2d	$⊢ v = 2^{nd} (Q (b)) \to ⟨suc b, b F v⟩ = ⟨suc b, b F 2^{nd} (Q (b))⟩$
43		eqid	$⊢ (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) = (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩)$
44		opex	$⊢ ⟨suc b, b F 2^{nd} (Q (b))⟩ \in V$
45	40 42 43 44	ovmpo	$⊢ (b \in ω \land 2^{nd} (Q (b)) \in V) \to b (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) 2^{nd} (Q (b)) = ⟨suc b, b F 2^{nd} (Q (b))⟩$
46	37 45	mpan2	$⊢ b \in ω \to b (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) 2^{nd} (Q (b)) = ⟨suc b, b F 2^{nd} (Q (b))⟩$
47	36 46	eqtr3id	$⊢ b \in ω \to (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (⟨b, 2^{nd} (Q (b))⟩) = ⟨suc b, b F 2^{nd} (Q (b))⟩$
48		fveqeq2	$⊢ Q (b) = ⟨b, 2^{nd} (Q (b))⟩ \to ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (Q (b)) = ⟨suc b, b F 2^{nd} (Q (b))⟩ \leftrightarrow (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (⟨b, 2^{nd} (Q (b))⟩) = ⟨suc b, b F 2^{nd} (Q (b))⟩)$
49	47 48	syl5ibrcom	$⊢ b \in ω \to (Q (b) = ⟨b, 2^{nd} (Q (b))⟩ \to (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (Q (b)) = ⟨suc b, b F 2^{nd} (Q (b))⟩)$
50		vex	$⊢ b \in V$
51	50	sucex	$⊢ suc b \in V$
52		ovex	$⊢ b F 2^{nd} (Q (b)) \in V$
53	51 52	op2nd	$⊢ 2^{nd} (⟨suc b, b F 2^{nd} (Q (b))⟩) = b F 2^{nd} (Q (b))$
54	53	eqcomi	$⊢ b F 2^{nd} (Q (b)) = 2^{nd} (⟨suc b, b F 2^{nd} (Q (b))⟩)$
55	54	a1i	$⊢ b \in ω \to b F 2^{nd} (Q (b)) = 2^{nd} (⟨suc b, b F 2^{nd} (Q (b))⟩)$
56	55	opeq2d	$⊢ b \in ω \to ⟨suc b, b F 2^{nd} (Q (b))⟩ = ⟨suc b, 2^{nd} (⟨suc b, b F 2^{nd} (Q (b))⟩)⟩$
57		id	$⊢ (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (Q (b)) = ⟨suc b, b F 2^{nd} (Q (b))⟩ \to (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (Q (b)) = ⟨suc b, b F 2^{nd} (Q (b))⟩$
58		fveq2	$⊢ (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (Q (b)) = ⟨suc b, b F 2^{nd} (Q (b))⟩ \to 2^{nd} ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (Q (b))) = 2^{nd} (⟨suc b, b F 2^{nd} (Q (b))⟩)$
59	58	opeq2d	$⊢ (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (Q (b)) = ⟨suc b, b F 2^{nd} (Q (b))⟩ \to ⟨suc b, 2^{nd} ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (Q (b)))⟩ = ⟨suc b, 2^{nd} (⟨suc b, b F 2^{nd} (Q (b))⟩)⟩$
60	57 59	eqeq12d	$⊢ (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (Q (b)) = ⟨suc b, b F 2^{nd} (Q (b))⟩ \to ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (Q (b)) = ⟨suc b, 2^{nd} ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (Q (b)))⟩ \leftrightarrow ⟨suc b, b F 2^{nd} (Q (b))⟩ = ⟨suc b, 2^{nd} (⟨suc b, b F 2^{nd} (Q (b))⟩)⟩)$
61	56 60	syl5ibrcom	$⊢ b \in ω \to ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (Q (b)) = ⟨suc b, b F 2^{nd} (Q (b))⟩ \to (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (Q (b)) = ⟨suc b, 2^{nd} ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (Q (b)))⟩)$
62	49 61	syld	$⊢ b \in ω \to (Q (b) = ⟨b, 2^{nd} (Q (b))⟩ \to (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (Q (b)) = ⟨suc b, 2^{nd} ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (Q (b)))⟩)$
63		frsuc	$⊢ b \in ω \to ({rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) ↾}_{ω}) (suc b) = (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (({rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) ↾}_{ω}) (b))$
64		peano2	$⊢ b \in ω \to suc b \in ω$
65	64	fvresd	$⊢ b \in ω \to ({rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) ↾}_{ω}) (suc b) = rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) (suc b)$
66	1	fveq1i	$⊢ Q (suc b) = rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) (suc b)$
67	65 66	eqtr4di	$⊢ b \in ω \to ({rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) ↾}_{ω}) (suc b) = Q (suc b)$
68		fvres	$⊢ b \in ω \to ({rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) ↾}_{ω}) (b) = rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) (b)$
69	1	fveq1i	$⊢ Q (b) = rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) (b)$
70	68 69	eqtr4di	$⊢ b \in ω \to ({rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) ↾}_{ω}) (b) = Q (b)$
71	70	fveq2d	$⊢ b \in ω \to (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (({rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) ↾}_{ω}) (b)) = (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (Q (b))$
72	63 67 71	3eqtr3d	$⊢ b \in ω \to Q (suc b) = (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (Q (b))$
73	72	fveq2d	$⊢ b \in ω \to 2^{nd} (Q (suc b)) = 2^{nd} ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (Q (b)))$
74	73	opeq2d	$⊢ b \in ω \to ⟨suc b, 2^{nd} (Q (suc b))⟩ = ⟨suc b, 2^{nd} ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (Q (b)))⟩$
75	72 74	eqeq12d	$⊢ b \in ω \to (Q (suc b) = ⟨suc b, 2^{nd} (Q (suc b))⟩ \leftrightarrow (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (Q (b)) = ⟨suc b, 2^{nd} ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (Q (b)))⟩)$
76	62 75	sylibrd	$⊢ b \in ω \to (Q (b) = ⟨b, 2^{nd} (Q (b))⟩ \to Q (suc b) = ⟨suc b, 2^{nd} (Q (suc b))⟩)$
77	6 11 16 21 35 76	finds	$⊢ A \in ω \to Q (A) = ⟨A, 2^{nd} (Q (A))⟩$

Metamath Proof Explorer

Theorem seqomlem1

Proof