Theorem infpssrlem1

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	infpssrlem1	⊢ ( 𝜑 → ( 𝐺 ‘ ∅ ) = 𝐶 )

Proof

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