Metamath Proof Explorer

Theorem noseqind

Description: Peano's inductive postulate for surreal sequences. (Contributed by Scott Fenton, 18-Apr-2025)

Ref Expression
Hypotheses noseq.1 ⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) “ ω ) )
noseq.2 ⊢ ( 𝜑 → 𝐴 ∈ No )
noseqind.3 ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
noseqind.4 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 +s 1s ) ∈ 𝐵 )
Assertion noseqind ( 𝜑 → 𝑍 ⊆ 𝐵 )

Proof

Step Hyp Ref Expression
1 noseq.1 ⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) “ ω ) )
2 noseq.2 ⊢ ( 𝜑 → 𝐴 ∈ No )
3 noseqind.3 ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
4 noseqind.4 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 +s 1s ) ∈ 𝐵 )
5 df-ima ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) “ ω ) = ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω )
6 1 5 eqtrdi ⊢ ( 𝜑 → 𝑍 = ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) )
7 fveq2 ⊢ ( 𝑧 = ∅ → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ ∅ ) )
8 7 eleq1d ⊢ ( 𝑧 = ∅ → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) ∈ 𝐵 ↔ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ ∅ ) ∈ 𝐵 ) )
9 fveq2 ⊢ ( 𝑧 = 𝑤 → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) )
10 9 eleq1d ⊢ ( 𝑧 = 𝑤 → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) ∈ 𝐵 ↔ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) ∈ 𝐵 ) )
11 fveq2 ⊢ ( 𝑧 = suc 𝑤 → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ suc 𝑤 ) )
12 11 eleq1d ⊢ ( 𝑧 = suc 𝑤 → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) ∈ 𝐵 ↔ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ suc 𝑤 ) ∈ 𝐵 ) )
13 fr0g ⊢ ( 𝐴 ∈ No → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ ∅ ) = 𝐴 )
14 2 13 syl ⊢ ( 𝜑 → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ ∅ ) = 𝐴 )
15 14 3 eqeltrd ⊢ ( 𝜑 → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ ∅ ) ∈ 𝐵 )
16 oveq1 ⊢ ( 𝑦 = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) → ( 𝑦 +s 1s ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) +s 1s ) )
17 16 eleq1d ⊢ ( 𝑦 = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) → ( ( 𝑦 +s 1s ) ∈ 𝐵 ↔ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) +s 1s ) ∈ 𝐵 ) )
18 17 imbi2d ⊢ ( 𝑦 = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) → ( ( 𝜑 → ( 𝑦 +s 1s ) ∈ 𝐵 ) ↔ ( 𝜑 → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) +s 1s ) ∈ 𝐵 ) ) )
19 4 expcom ⊢ ( 𝑦 ∈ 𝐵 → ( 𝜑 → ( 𝑦 +s 1s ) ∈ 𝐵 ) )
20 18 19 vtoclga ⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) ∈ 𝐵 → ( 𝜑 → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) +s 1s ) ∈ 𝐵 ) )
21 20 impcom ⊢ ( ( 𝜑 ∧ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) ∈ 𝐵 ) → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) +s 1s ) ∈ 𝐵 )
22 ovex ⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) +s 1s ) ∈ V
23 eqid ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω )
24 oveq1 ⊢ ( 𝑡 = 𝑥 → ( 𝑡 +s 1s ) = ( 𝑥 +s 1s ) )
25 oveq1 ⊢ ( 𝑡 = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) → ( 𝑡 +s 1s ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) +s 1s ) )
26 23 24 25 frsucmpt2 ⊢ ( ( 𝑤 ∈ ω ∧ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) +s 1s ) ∈ V ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ suc 𝑤 ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) +s 1s ) )
27 22 26 mpan2 ⊢ ( 𝑤 ∈ ω → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ suc 𝑤 ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) +s 1s ) )
28 27 eleq1d ⊢ ( 𝑤 ∈ ω → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ suc 𝑤 ) ∈ 𝐵 ↔ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) +s 1s ) ∈ 𝐵 ) )
29 21 28 imbitrrid ⊢ ( 𝑤 ∈ ω → ( ( 𝜑 ∧ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) ∈ 𝐵 ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ suc 𝑤 ) ∈ 𝐵 ) )
30 29 expd ⊢ ( 𝑤 ∈ ω → ( 𝜑 → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) ∈ 𝐵 → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ suc 𝑤 ) ∈ 𝐵 ) ) )
31 8 10 12 15 30 finds2 ⊢ ( 𝑧 ∈ ω → ( 𝜑 → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) ∈ 𝐵 ) )
32 31 com12 ⊢ ( 𝜑 → ( 𝑧 ∈ ω → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) ∈ 𝐵 ) )
33 32 ralrimiv ⊢ ( 𝜑 → ∀ 𝑧 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) ∈ 𝐵 )
34 frfnom ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) Fn ω
35 ffnfv ⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) : ω ⟶ 𝐵 ↔ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) Fn ω ∧ ∀ 𝑧 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) ∈ 𝐵 ) )
36 34 35 mpbiran ⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) : ω ⟶ 𝐵 ↔ ∀ 𝑧 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) ∈ 𝐵 )
37 33 36 sylibr ⊢ ( 𝜑 → ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) : ω ⟶ 𝐵 )
38 37 frnd ⊢ ( 𝜑 → ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ⊆ 𝐵 )
39 6 38 eqsstrd ⊢ ( 𝜑 → 𝑍 ⊆ 𝐵 )