Metamath Proof Explorer

Theorem infpssrlem2

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

Ref Expression
Hypotheses infpssrlem.a ⊢ φ → B ⊆ A
infpssrlem.c ⊢ φ → F : B ⟶ 1-1 onto A
infpssrlem.d ⊢ φ → C ∈ A ∖ B
infpssrlem.e ⊢ G = rec ⁡ F -1 C ↾ ω
Assertion infpssrlem2 ⊢ M ∈ ω → G ⁡ suc ⁡ M = F -1 ⁡ G ⁡ M

Proof

Step Hyp Ref Expression
1 infpssrlem.a ⊢ φ → B ⊆ A
2 infpssrlem.c ⊢ φ → F : B ⟶ 1-1 onto A
3 infpssrlem.d ⊢ φ → C ∈ A ∖ B
4 infpssrlem.e ⊢ G = rec ⁡ F -1 C ↾ ω
5 frsuc ⊢ M ∈ ω → rec ⁡ F -1 C ↾ ω ⁡ suc ⁡ M = F -1 ⁡ rec ⁡ F -1 C ↾ ω ⁡ M
6 4 fveq1i ⊢ G ⁡ suc ⁡ M = rec ⁡ F -1 C ↾ ω ⁡ suc ⁡ M
7 4 fveq1i ⊢ G ⁡ M = rec ⁡ F -1 C ↾ ω ⁡ M
8 7 fveq2i ⊢ F -1 ⁡ G ⁡ M = F -1 ⁡ rec ⁡ F -1 C ↾ ω ⁡ M
9 5 6 8 3eqtr4g ⊢ M ∈ ω → G ⁡ suc ⁡ M = F -1 ⁡ G ⁡ M