Theorem infpssrlem3

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	infpssrlem3	⊢ ( 𝜑 → 𝐺 : ω ⟶ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		infpssrlem.a	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
2		infpssrlem.c	⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1-onto→ 𝐴 )
3		infpssrlem.d	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 ∖ 𝐵 ) )
4		infpssrlem.e	⊢ 𝐺 = ( rec ( ◡ 𝐹 , 𝐶 ) ↾ ω )
5		frfnom	⊢ ( rec ( ◡ 𝐹 , 𝐶 ) ↾ ω ) Fn ω
6	4	fneq1i	⊢ ( 𝐺 Fn ω ↔ ( rec ( ◡ 𝐹 , 𝐶 ) ↾ ω ) Fn ω )
7	5 6	mpbir	⊢ 𝐺 Fn ω
8	7	a1i	⊢ ( 𝜑 → 𝐺 Fn ω )
9		fveq2	⊢ ( 𝑐 = ∅ → ( 𝐺 ‘ 𝑐 ) = ( 𝐺 ‘ ∅ ) )
10	9	eleq1d	⊢ ( 𝑐 = ∅ → ( ( 𝐺 ‘ 𝑐 ) ∈ 𝐴 ↔ ( 𝐺 ‘ ∅ ) ∈ 𝐴 ) )
11		fveq2	⊢ ( 𝑐 = 𝑏 → ( 𝐺 ‘ 𝑐 ) = ( 𝐺 ‘ 𝑏 ) )
12	11	eleq1d	⊢ ( 𝑐 = 𝑏 → ( ( 𝐺 ‘ 𝑐 ) ∈ 𝐴 ↔ ( 𝐺 ‘ 𝑏 ) ∈ 𝐴 ) )
13		fveq2	⊢ ( 𝑐 = suc 𝑏 → ( 𝐺 ‘ 𝑐 ) = ( 𝐺 ‘ suc 𝑏 ) )
14	13	eleq1d	⊢ ( 𝑐 = suc 𝑏 → ( ( 𝐺 ‘ 𝑐 ) ∈ 𝐴 ↔ ( 𝐺 ‘ suc 𝑏 ) ∈ 𝐴 ) )
15	1 2 3 4	infpssrlem1	⊢ ( 𝜑 → ( 𝐺 ‘ ∅ ) = 𝐶 )
16	3	eldifad	⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
17	15 16	eqeltrd	⊢ ( 𝜑 → ( 𝐺 ‘ ∅ ) ∈ 𝐴 )
18	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑏 ) ∈ 𝐴 ) → 𝐵 ⊆ 𝐴 )
19		f1ocnv	⊢ ( 𝐹 : 𝐵 –1-1-onto→ 𝐴 → ◡ 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
20		f1of	⊢ ( ◡ 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ◡ 𝐹 : 𝐴 ⟶ 𝐵 )
21	2 19 20	3syl	⊢ ( 𝜑 → ◡ 𝐹 : 𝐴 ⟶ 𝐵 )
22	21	ffvelcdmda	⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑏 ) ∈ 𝐴 ) → ( ◡ 𝐹 ‘ ( 𝐺 ‘ 𝑏 ) ) ∈ 𝐵 )
23	18 22	sseldd	⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑏 ) ∈ 𝐴 ) → ( ◡ 𝐹 ‘ ( 𝐺 ‘ 𝑏 ) ) ∈ 𝐴 )
24	1 2 3 4	infpssrlem2	⊢ ( 𝑏 ∈ ω → ( 𝐺 ‘ suc 𝑏 ) = ( ◡ 𝐹 ‘ ( 𝐺 ‘ 𝑏 ) ) )
25	24	eleq1d	⊢ ( 𝑏 ∈ ω → ( ( 𝐺 ‘ suc 𝑏 ) ∈ 𝐴 ↔ ( ◡ 𝐹 ‘ ( 𝐺 ‘ 𝑏 ) ) ∈ 𝐴 ) )
26	23 25	imbitrrid	⊢ ( 𝑏 ∈ ω → ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑏 ) ∈ 𝐴 ) → ( 𝐺 ‘ suc 𝑏 ) ∈ 𝐴 ) )
27	26	expd	⊢ ( 𝑏 ∈ ω → ( 𝜑 → ( ( 𝐺 ‘ 𝑏 ) ∈ 𝐴 → ( 𝐺 ‘ suc 𝑏 ) ∈ 𝐴 ) ) )
28	10 12 14 17 27	finds2	⊢ ( 𝑐 ∈ ω → ( 𝜑 → ( 𝐺 ‘ 𝑐 ) ∈ 𝐴 ) )
29	28	com12	⊢ ( 𝜑 → ( 𝑐 ∈ ω → ( 𝐺 ‘ 𝑐 ) ∈ 𝐴 ) )
30	29	ralrimiv	⊢ ( 𝜑 → ∀ 𝑐 ∈ ω ( 𝐺 ‘ 𝑐 ) ∈ 𝐴 )
31		ffnfv	⊢ ( 𝐺 : ω ⟶ 𝐴 ↔ ( 𝐺 Fn ω ∧ ∀ 𝑐 ∈ ω ( 𝐺 ‘ 𝑐 ) ∈ 𝐴 ) )
32	8 30 31	sylanbrc	⊢ ( 𝜑 → 𝐺 : ω ⟶ 𝐴 )