This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐼 )