Metamath Proof Explorer


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