Metamath Proof Explorer

Theorem noseqrdglem

Description: A helper lemma for the value of a recursive defintion generator on surreal sequences. (Contributed by Scott Fenton, 18-Apr-2025)

Ref Expression
Hypotheses om2noseq.1 ⊢ ( 𝜑 → 𝐶 ∈ No )
om2noseq.2 ⊢ ( 𝜑 → 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) )
om2noseq.3 ⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) “ ω ) )
noseqrdg.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
noseqrdg.2 ⊢ ( 𝜑 → 𝑅 = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) )
Assertion noseqrdglem ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ⟨ 𝐵 , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ⟩ ∈ ran 𝑅 )

Proof

Step Hyp Ref Expression
1 om2noseq.1 ⊢ ( 𝜑 → 𝐶 ∈ No )
2 om2noseq.2 ⊢ ( 𝜑 → 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) )
3 om2noseq.3 ⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) “ ω ) )
4 noseqrdg.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5 noseqrdg.2 ⊢ ( 𝜑 → 𝑅 = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) )
6 1 2 3 om2noseqf1o ⊢ ( 𝜑 → 𝐺 : ω –1-1-onto→ 𝑍 )
7 f1ocnvdm ⊢ ( ( 𝐺 : ω –1-1-onto→ 𝑍 ∧ 𝐵 ∈ 𝑍 ) → ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω )
8 6 7 sylan ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω )
9 1 2 3 4 5 om2noseqrdg ⊢ ( ( 𝜑 ∧ ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω ) → ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) = ⟨ ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ⟩ )
10 8 9 syldan ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) = ⟨ ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ⟩ )
11 f1ocnvfv2 ⊢ ( ( 𝐺 : ω –1-1-onto→ 𝑍 ∧ 𝐵 ∈ 𝑍 ) → ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) = 𝐵 )
12 6 11 sylan ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) = 𝐵 )
13 12 opeq1d ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ⟨ ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ⟩ = ⟨ 𝐵 , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ⟩ )
14 10 13 eqtrd ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) = ⟨ 𝐵 , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ⟩ )
15 frfnom ⊢ ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) Fn ω
16 5 fneq1d ⊢ ( 𝜑 → ( 𝑅 Fn ω ↔ ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) Fn ω ) )
17 15 16 mpbiri ⊢ ( 𝜑 → 𝑅 Fn ω )
18 17 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → 𝑅 Fn ω )
19 18 8 fnfvelrnd ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ∈ ran 𝑅 )
20 14 19 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ⟨ 𝐵 , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ⟩ ∈ ran 𝑅 )