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 𝑀 ) = ( ◡ 𝐹 ‘ ( 𝐺 ‘ 𝑀 ) ) )