This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem infpssrlem1

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 infpssrlem1 ⊢ φ → G ⁡ ∅ = C

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 4 fveq1i ⊢ G ⁡ ∅ = rec ⁡ F -1 C ↾ ω ⁡ ∅
6 fr0g ⊢ C ∈ A ∖ B → rec ⁡ F -1 C ↾ ω ⁡ ∅ = C
7 3 6 syl ⊢ φ → rec ⁡ F -1 C ↾ ω ⁡ ∅ = C
8 5 7 eqtrid ⊢ φ → G ⁡ ∅ = C