Metamath Proof Explorer

Theorem infpssrlem3

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 infpssrlem3 ⊢ φ → G : ω ⟶ A

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 frfnom ⊢ rec ⁡ F -1 C ↾ ω Fn ω
6 4 fneq1i ⊢ G Fn ω ↔ rec ⁡ F -1 C ↾ ω Fn ω
7 5 6 mpbir ⊢ G Fn ω
8 7 a1i ⊢ φ → G Fn ω
9 fveq2 ⊢ c = ∅ → G ⁡ c = G ⁡ ∅
10 9 eleq1d ⊢ c = ∅ → G ⁡ c ∈ A ↔ G ⁡ ∅ ∈ A
11 fveq2 ⊢ c = b → G ⁡ c = G ⁡ b
12 11 eleq1d ⊢ c = b → G ⁡ c ∈ A ↔ G ⁡ b ∈ A
13 fveq2 ⊢ c = suc ⁡ b → G ⁡ c = G ⁡ suc ⁡ b
14 13 eleq1d ⊢ c = suc ⁡ b → G ⁡ c ∈ A ↔ G ⁡ suc ⁡ b ∈ A
15 1 2 3 4 infpssrlem1 ⊢ φ → G ⁡ ∅ = C
16 3 eldifad ⊢ φ → C ∈ A
17 15 16 eqeltrd ⊢ φ → G ⁡ ∅ ∈ A
18 1 adantr ⊢ φ ∧ G ⁡ b ∈ A → B ⊆ A
19 f1ocnv ⊢ F : B ⟶ 1-1 onto A → F -1 : A ⟶ 1-1 onto B
20 f1of ⊢ F -1 : A ⟶ 1-1 onto B → F -1 : A ⟶ B
21 2 19 20 3syl ⊢ φ → F -1 : A ⟶ B
22 21 ffvelcdmda ⊢ φ ∧ G ⁡ b ∈ A → F -1 ⁡ G ⁡ b ∈ B
23 18 22 sseldd ⊢ φ ∧ G ⁡ b ∈ A → F -1 ⁡ G ⁡ b ∈ A
24 1 2 3 4 infpssrlem2 ⊢ b ∈ ω → G ⁡ suc ⁡ b = F -1 ⁡ G ⁡ b
25 24 eleq1d ⊢ b ∈ ω → G ⁡ suc ⁡ b ∈ A ↔ F -1 ⁡ G ⁡ b ∈ A
26 23 25 imbitrrid ⊢ b ∈ ω → φ ∧ G ⁡ b ∈ A → G ⁡ suc ⁡ b ∈ A
27 26 expd ⊢ b ∈ ω → φ → G ⁡ b ∈ A → G ⁡ suc ⁡ b ∈ A
28 10 12 14 17 27 finds2 ⊢ c ∈ ω → φ → G ⁡ c ∈ A
29 28 com12 ⊢ φ → c ∈ ω → G ⁡ c ∈ A
30 29 ralrimiv ⊢ φ → ∀ c ∈ ω G ⁡ c ∈ A
31 ffnfv ⊢ G : ω ⟶ A ↔ G Fn ω ∧ ∀ c ∈ ω G ⁡ c ∈ A
32 8 30 31 sylanbrc ⊢ φ → G : ω ⟶ A