Metamath Proof Explorer


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 ffvelrnda ( ( 𝜑 ∧ ( 𝐺𝑏 ) ∈ 𝐴 ) → ( 𝐹 ‘ ( 𝐺𝑏 ) ) ∈ 𝐵 )
23 18 22 sseldd ( ( 𝜑 ∧ ( 𝐺𝑏 ) ∈ 𝐴 ) → ( 𝐹 ‘ ( 𝐺𝑏 ) ) ∈ 𝐴 )
24 1 2 3 4 infpssrlem2 ( 𝑏 ∈ ω → ( 𝐺 ‘ suc 𝑏 ) = ( 𝐹 ‘ ( 𝐺𝑏 ) ) )
25 24 eleq1d ( 𝑏 ∈ ω → ( ( 𝐺 ‘ suc 𝑏 ) ∈ 𝐴 ↔ ( 𝐹 ‘ ( 𝐺𝑏 ) ) ∈ 𝐴 ) )
26 23 25 syl5ibr ( 𝑏 ∈ ω → ( ( 𝜑 ∧ ( 𝐺𝑏 ) ∈ 𝐴 ) → ( 𝐺 ‘ 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 ( 𝜑𝐺 : ω ⟶ 𝐴 )