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

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