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

Metamath Proof Explorer

Theorem infpssrlem2

Description: Lemma for infpssr . (Contributed by Stefan O'Rear, 30-Oct-2014)

Ref Expression
Hypotheses infpssrlem.a ⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
infpssrlem.c ⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1-onto→ 𝐴 )
infpssrlem.d ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 ∖ 𝐵 ) )
infpssrlem.e ⊢ 𝐺 = ( rec ( ◡ 𝐹 , 𝐶 ) ↾ ω )
Assertion infpssrlem2 ( 𝑀 ∈ ω → ( 𝐺 ‘ suc 𝑀 ) = ( ◡ 𝐹 ‘ ( 𝐺 ‘ 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 infpssrlem.a ⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
2 infpssrlem.c ⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1-onto→ 𝐴 )
3 infpssrlem.d ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 ∖ 𝐵 ) )
4 infpssrlem.e ⊢ 𝐺 = ( rec ( ◡ 𝐹 , 𝐶 ) ↾ ω )
5 frsuc ⊢ ( 𝑀 ∈ ω → ( ( rec ( ◡ 𝐹 , 𝐶 ) ↾ ω ) ‘ suc 𝑀 ) = ( ◡ 𝐹 ‘ ( ( rec ( ◡ 𝐹 , 𝐶 ) ↾ ω ) ‘ 𝑀 ) ) )
6 4 fveq1i ⊢ ( 𝐺 ‘ suc 𝑀 ) = ( ( rec ( ◡ 𝐹 , 𝐶 ) ↾ ω ) ‘ suc 𝑀 )
7 4 fveq1i ⊢ ( 𝐺 ‘ 𝑀 ) = ( ( rec ( ◡ 𝐹 , 𝐶 ) ↾ ω ) ‘ 𝑀 )
8 7 fveq2i ⊢ ( ◡ 𝐹 ‘ ( 𝐺 ‘ 𝑀 ) ) = ( ◡ 𝐹 ‘ ( ( rec ( ◡ 𝐹 , 𝐶 ) ↾ ω ) ‘ 𝑀 ) )
9 5 6 8 3eqtr4g ⊢ ( 𝑀 ∈ ω → ( 𝐺 ‘ suc 𝑀 ) = ( ◡ 𝐹 ‘ ( 𝐺 ‘ 𝑀 ) ) )