Theorem seqomlem3

Description: Lemma for seqom . (Contributed by Stefan O'Rear, 1-Nov-2014)

	Ref	Expression
Hypothesis	seqomlem.a	⊢ 𝑄 = rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ )
Assertion	seqomlem3	⊢ ( ( 𝑄 “ ω ) ‘ ∅ ) = ( I ‘ 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		seqomlem.a	⊢ 𝑄 = rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ )
2		peano1	⊢ ∅ ∈ ω
3		fvres	⊢ ( ∅ ∈ ω → ( ( 𝑄 ↾ ω ) ‘ ∅ ) = ( 𝑄 ‘ ∅ ) )
4	2 3	ax-mp	⊢ ( ( 𝑄 ↾ ω ) ‘ ∅ ) = ( 𝑄 ‘ ∅ )
5	1	fveq1i	⊢ ( 𝑄 ‘ ∅ ) = ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ‘ ∅ )
6		opex	⊢ ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ∈ V
7	6	rdg0	⊢ ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ‘ ∅ ) = ⟨ ∅ , ( I ‘ 𝐼 ) ⟩
8	4 5 7	3eqtri	⊢ ( ( 𝑄 ↾ ω ) ‘ ∅ ) = ⟨ ∅ , ( I ‘ 𝐼 ) ⟩
9		frfnom	⊢ ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ↾ ω ) Fn ω
10	1	reseq1i	⊢ ( 𝑄 ↾ ω ) = ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ↾ ω )
11	10	fneq1i	⊢ ( ( 𝑄 ↾ ω ) Fn ω ↔ ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ↾ ω ) Fn ω )
12	9 11	mpbir	⊢ ( 𝑄 ↾ ω ) Fn ω
13		fnfvelrn	⊢ ( ( ( 𝑄 ↾ ω ) Fn ω ∧ ∅ ∈ ω ) → ( ( 𝑄 ↾ ω ) ‘ ∅ ) ∈ ran ( 𝑄 ↾ ω ) )
14	12 2 13	mp2an	⊢ ( ( 𝑄 ↾ ω ) ‘ ∅ ) ∈ ran ( 𝑄 ↾ ω )
15	8 14	eqeltrri	⊢ ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ∈ ran ( 𝑄 ↾ ω )
16		df-ima	⊢ ( 𝑄 “ ω ) = ran ( 𝑄 ↾ ω )
17	15 16	eleqtrri	⊢ ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ∈ ( 𝑄 “ ω )
18		df-br	⊢ ( ∅ ( 𝑄 “ ω ) ( I ‘ 𝐼 ) ↔ ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ∈ ( 𝑄 “ ω ) )
19	17 18	mpbir	⊢ ∅ ( 𝑄 “ ω ) ( I ‘ 𝐼 )
20	1	seqomlem2	⊢ ( 𝑄 “ ω ) Fn ω
21		fnbrfvb	⊢ ( ( ( 𝑄 “ ω ) Fn ω ∧ ∅ ∈ ω ) → ( ( ( 𝑄 “ ω ) ‘ ∅ ) = ( I ‘ 𝐼 ) ↔ ∅ ( 𝑄 “ ω ) ( I ‘ 𝐼 ) ) )
22	20 2 21	mp2an	⊢ ( ( ( 𝑄 “ ω ) ‘ ∅ ) = ( I ‘ 𝐼 ) ↔ ∅ ( 𝑄 “ ω ) ( I ‘ 𝐼 ) )
23	19 22	mpbir	⊢ ( ( 𝑄 “ ω ) ‘ ∅ ) = ( I ‘ 𝐼 )