seqomlem4

Description: Lemma for seqom . (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	seqomlem4	$⊢ A \in ω \to Q [ω] (suc A) = A F 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		peano2	$⊢ A \in ω \to suc A \in ω$
3	2	fvresd	$⊢ A \in ω \to ({Q ↾}_{ω}) (suc A) = Q (suc A)$
4		frsuc	$⊢ A \in ω \to ({rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) ↾}_{ω}) (suc A) = (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (({rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) ↾}_{ω}) (A))$
5	2	fvresd	$⊢ A \in ω \to ({rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) ↾}_{ω}) (suc A) = rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) (suc A)$
6	1	fveq1i	$⊢ Q (suc A) = rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) (suc A)$
7	5 6	eqtr4di	$⊢ A \in ω \to ({rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) ↾}_{ω}) (suc A) = Q (suc A)$
8		fvres	$⊢ A \in ω \to ({rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) ↾}_{ω}) (A) = rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) (A)$
9	1	fveq1i	$⊢ Q (A) = rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) (A)$
10	8 9	eqtr4di	$⊢ A \in ω \to ({rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) ↾}_{ω}) (A) = Q (A)$
11	10	fveq2d	$⊢ A \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)⟩) ↾}_{ω}) (A)) = (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (Q (A))$
12	4 7 11	3eqtr3d	$⊢ A \in ω \to Q (suc A) = (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (Q (A))$
13	1	seqomlem1	$⊢ A \in ω \to Q (A) = ⟨A, 2^{nd} (Q (A))⟩$
14	13	fveq2d	$⊢ A \in ω \to (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (Q (A)) = (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (⟨A, 2^{nd} (Q (A))⟩)$
15		df-ov	$⊢ A (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) 2^{nd} (Q (A)) = (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (⟨A, 2^{nd} (Q (A))⟩)$
16		fvex	$⊢ 2^{nd} (Q (A)) \in V$
17		suceq	$⊢ i = A \to suc i = suc A$
18		oveq1	$⊢ i = A \to i F v = A F v$
19	17 18	opeq12d	$⊢ i = A \to ⟨suc i, i F v⟩ = ⟨suc A, A F v⟩$
20		oveq2	$⊢ v = 2^{nd} (Q (A)) \to A F v = A F 2^{nd} (Q (A))$
21	20	opeq2d	$⊢ v = 2^{nd} (Q (A)) \to ⟨suc A, A F v⟩ = ⟨suc A, A F 2^{nd} (Q (A))⟩$
22		eqid	$⊢ (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) = (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩)$
23		opex	$⊢ ⟨suc A, A F 2^{nd} (Q (A))⟩ \in V$
24	19 21 22 23	ovmpo	$⊢ (A \in ω \land 2^{nd} (Q (A)) \in V) \to A (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) 2^{nd} (Q (A)) = ⟨suc A, A F 2^{nd} (Q (A))⟩$
25	16 24	mpan2	$⊢ A \in ω \to A (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) 2^{nd} (Q (A)) = ⟨suc A, A F 2^{nd} (Q (A))⟩$
26		fvres	$⊢ A \in ω \to ({Q ↾}_{ω}) (A) = Q (A)$
27	26 13	eqtrd	$⊢ A \in ω \to ({Q ↾}_{ω}) (A) = ⟨A, 2^{nd} (Q (A))⟩$
28		frfnom	$⊢ ({rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) ↾}_{ω}) Fn ω$
29	1	reseq1i	$⊢ {Q ↾}_{ω} = {rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) ↾}_{ω}$
30	29	fneq1i	$⊢ ({Q ↾}_{ω}) Fn ω \leftrightarrow ({rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) ↾}_{ω}) Fn ω$
31	28 30	mpbir	$⊢ ({Q ↾}_{ω}) Fn ω$
32		fnfvelrn	$⊢ (({Q ↾}_{ω}) Fn ω \land A \in ω) \to ({Q ↾}_{ω}) (A) \in ran ({Q ↾}_{ω})$
33	31 32	mpan	$⊢ A \in ω \to ({Q ↾}_{ω}) (A) \in ran ({Q ↾}_{ω})$
34	27 33	eqeltrrd	$⊢ A \in ω \to ⟨A, 2^{nd} (Q (A))⟩ \in ran ({Q ↾}_{ω})$
35		df-ima	$⊢ Q [ω] = ran ({Q ↾}_{ω})$
36	34 35	eleqtrrdi	$⊢ A \in ω \to ⟨A, 2^{nd} (Q (A))⟩ \in Q [ω]$
37		df-br	$⊢ A Q [ω] 2^{nd} (Q (A)) \leftrightarrow ⟨A, 2^{nd} (Q (A))⟩ \in Q [ω]$
38	36 37	sylibr	$⊢ A \in ω \to A Q [ω] 2^{nd} (Q (A))$
39	1	seqomlem2	$⊢ Q [ω] Fn ω$
40		fnbrfvb	$⊢ (Q [ω] Fn ω \land A \in ω) \to (Q [ω] (A) = 2^{nd} (Q (A)) \leftrightarrow A Q [ω] 2^{nd} (Q (A)))$
41	39 40	mpan	$⊢ A \in ω \to (Q [ω] (A) = 2^{nd} (Q (A)) \leftrightarrow A Q [ω] 2^{nd} (Q (A)))$
42	38 41	mpbird	$⊢ A \in ω \to Q [ω] (A) = 2^{nd} (Q (A))$
43	42	eqcomd	$⊢ A \in ω \to 2^{nd} (Q (A)) = Q [ω] (A)$
44	43	oveq2d	$⊢ A \in ω \to A F 2^{nd} (Q (A)) = A F Q [ω] (A)$
45	44	opeq2d	$⊢ A \in ω \to ⟨suc A, A F 2^{nd} (Q (A))⟩ = ⟨suc A, A F Q [ω] (A)⟩$
46	25 45	eqtrd	$⊢ A \in ω \to A (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) 2^{nd} (Q (A)) = ⟨suc A, A F Q [ω] (A)⟩$
47	15 46	eqtr3id	$⊢ A \in ω \to (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩) (⟨A, 2^{nd} (Q (A))⟩) = ⟨suc A, A F Q [ω] (A)⟩$
48	12 14 47	3eqtrd	$⊢ A \in ω \to Q (suc A) = ⟨suc A, A F Q [ω] (A)⟩$
49	3 48	eqtrd	$⊢ A \in ω \to ({Q ↾}_{ω}) (suc A) = ⟨suc A, A F Q [ω] (A)⟩$
50		fnfvelrn	$⊢ (({Q ↾}_{ω}) Fn ω \land suc A \in ω) \to ({Q ↾}_{ω}) (suc A) \in ran ({Q ↾}_{ω})$
51	31 2 50	sylancr	$⊢ A \in ω \to ({Q ↾}_{ω}) (suc A) \in ran ({Q ↾}_{ω})$
52	49 51	eqeltrrd	$⊢ A \in ω \to ⟨suc A, A F Q [ω] (A)⟩ \in ran ({Q ↾}_{ω})$
53	52 35	eleqtrrdi	$⊢ A \in ω \to ⟨suc A, A F Q [ω] (A)⟩ \in Q [ω]$
54		df-br	$⊢ suc A Q [ω] (A F Q [ω] (A)) \leftrightarrow ⟨suc A, A F Q [ω] (A)⟩ \in Q [ω]$
55	53 54	sylibr	$⊢ A \in ω \to suc A Q [ω] (A F Q [ω] (A))$
56		fnbrfvb	$⊢ (Q [ω] Fn ω \land suc A \in ω) \to (Q [ω] (suc A) = A F Q [ω] (A) \leftrightarrow suc A Q [ω] (A F Q [ω] (A)))$
57	39 2 56	sylancr	$⊢ A \in ω \to (Q [ω] (suc A) = A F Q [ω] (A) \leftrightarrow suc A Q [ω] (A F Q [ω] (A)))$
58	55 57	mpbird	$⊢ A \in ω \to Q [ω] (suc A) = A F Q [ω] (A)$

Metamath Proof Explorer

Theorem seqomlem4

Proof