Theorem om2noseqiso

Description: G is an isomorphism from the finite ordinals to a surreal sequence. (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 ) ) , 𝐶 ) “ ω ) )
Assertion	om2noseqiso	⊢ ( 𝜑 → 𝐺 Isom E , <s ( ω , 𝑍 ) )

Proof

Step	Hyp	Ref	Expression
1		om2noseq.1	⊢ ( 𝜑 → 𝐶 ∈ No )
2		om2noseq.2	⊢ ( 𝜑 → 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) )
3		om2noseq.3	⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) “ ω ) )
4	1 2 3	om2noseqf1o	⊢ ( 𝜑 → 𝐺 : ω –1-1-onto→ 𝑍 )
5		epel	⊢ ( 𝑦 E 𝑧 ↔ 𝑦 ∈ 𝑧 )
6	1 2 3	om2noseqlt2	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) ) → ( 𝑦 ∈ 𝑧 ↔ ( 𝐺 ‘ 𝑦 ) <s ( 𝐺 ‘ 𝑧 ) ) )
7	5 6	bitrid	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) ) → ( 𝑦 E 𝑧 ↔ ( 𝐺 ‘ 𝑦 ) <s ( 𝐺 ‘ 𝑧 ) ) )
8	7	ralrimivva	⊢ ( 𝜑 → ∀ 𝑦 ∈ ω ∀ 𝑧 ∈ ω ( 𝑦 E 𝑧 ↔ ( 𝐺 ‘ 𝑦 ) <s ( 𝐺 ‘ 𝑧 ) ) )
9		df-isom	⊢ ( 𝐺 Isom E , <s ( ω , 𝑍 ) ↔ ( 𝐺 : ω –1-1-onto→ 𝑍 ∧ ∀ 𝑦 ∈ ω ∀ 𝑧 ∈ ω ( 𝑦 E 𝑧 ↔ ( 𝐺 ‘ 𝑦 ) <s ( 𝐺 ‘ 𝑧 ) ) ) )
10	4 8 9	sylanbrc	⊢ ( 𝜑 → 𝐺 Isom E , <s ( ω , 𝑍 ) )