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