seqomlem3

		Ref	Expression
	Hypothesis	seqomlem.a	$⊢ Q = rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩)$
	Assertion	seqomlem3	$⊢ Q [ω] (\emptyset) = I (I)$

Proof

Step	Hyp	Ref	Expression
1		seqomlem.a	$⊢ Q = rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩)$
2		peano1	$⊢ \emptyset \in ω$
3		fvres	$⊢ \emptyset \in ω \to ({Q ↾}_{ω}) (\emptyset) = Q (\emptyset)$
4	2 3	ax-mp	$⊢ ({Q ↾}_{ω}) (\emptyset) = Q (\emptyset)$
5	1	fveq1i	$⊢ Q (\emptyset) = rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) (\emptyset)$
6		opex	$⊢ ⟨\emptyset, I (I)⟩ \in V$
7	6	rdg0	$⊢ rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) (\emptyset) = ⟨\emptyset, I (I)⟩$
8	4 5 7	3eqtri	$⊢ ({Q ↾}_{ω}) (\emptyset) = ⟨\emptyset, I (I)⟩$
9		frfnom	$⊢ ({rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) ↾}_{ω}) Fn ω$
10	1	reseq1i	$⊢ {Q ↾}_{ω} = {rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) ↾}_{ω}$
11	10	fneq1i	$⊢ ({Q ↾}_{ω}) Fn ω \leftrightarrow ({rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) ↾}_{ω}) Fn ω$
12	9 11	mpbir	$⊢ ({Q ↾}_{ω}) Fn ω$
13		fnfvelrn	$⊢ (({Q ↾}_{ω}) Fn ω \land \emptyset \in ω) \to ({Q ↾}_{ω}) (\emptyset) \in ran ({Q ↾}_{ω})$
14	12 2 13	mp2an	$⊢ ({Q ↾}_{ω}) (\emptyset) \in ran ({Q ↾}_{ω})$
15	8 14	eqeltrri	$⊢ ⟨\emptyset, I (I)⟩ \in ran ({Q ↾}_{ω})$
16		df-ima	$⊢ Q [ω] = ran ({Q ↾}_{ω})$
17	15 16	eleqtrri	$⊢ ⟨\emptyset, I (I)⟩ \in Q [ω]$
18		df-br	$⊢ \emptyset Q [ω] I (I) \leftrightarrow ⟨\emptyset, I (I)⟩ \in Q [ω]$
19	17 18	mpbir	$⊢ \emptyset Q [ω] I (I)$
20	1	seqomlem2	$⊢ Q [ω] Fn ω$
21		fnbrfvb	$⊢ (Q [ω] Fn ω \land \emptyset \in ω) \to (Q [ω] (\emptyset) = I (I) \leftrightarrow \emptyset Q [ω] I (I))$
22	20 2 21	mp2an	$⊢ Q [ω] (\emptyset) = I (I) \leftrightarrow \emptyset Q [ω] I (I)$
23	19 22	mpbir	$⊢ Q [ω] (\emptyset) = I (I)$

Metamath Proof Explorer

Theorem seqomlem3

Proof