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 
|- ( ph -> Z = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) " _om ) )
noseq.2 
|- ( ph -> A e. No )
noseqind.3 
|- ( ph -> A e. B )
noseqind.4 
|- ( ( ph /\ y e. B ) -> ( y +s 1s ) e. B )
Assertion noseqind 
|- ( ph -> Z C_ B )

Proof

Step Hyp Ref Expression
1 noseq.1 
 |-  ( ph -> Z = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) " _om ) )
2 noseq.2 
 |-  ( ph -> A e. No )
3 noseqind.3 
 |-  ( ph -> A e. B )
4 noseqind.4 
 |-  ( ( ph /\ y e. B ) -> ( y +s 1s ) e. B )
5 df-ima 
 |-  ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) " _om ) = ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om )
6 1 5 eqtrdi 
 |-  ( ph -> Z = ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) )
7 fveq2 
 |-  ( z = (/) -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` z ) = ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` (/) ) )
8 7 eleq1d 
 |-  ( z = (/) -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` z ) e. B <-> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` (/) ) e. B ) )
9 fveq2 
 |-  ( z = w -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` z ) = ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` w ) )
10 9 eleq1d 
 |-  ( z = w -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` z ) e. B <-> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` w ) e. B ) )
11 fveq2 
 |-  ( z = suc w -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` z ) = ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` suc w ) )
12 11 eleq1d 
 |-  ( z = suc w -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` z ) e. B <-> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` suc w ) e. B ) )
13 fr0g 
 |-  ( A e. No -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` (/) ) = A )
14 2 13 syl 
 |-  ( ph -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` (/) ) = A )
15 14 3 eqeltrd 
 |-  ( ph -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` (/) ) e. B )
16 oveq1 
 |-  ( y = ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` w ) -> ( y +s 1s ) = ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` w ) +s 1s ) )
17 16 eleq1d 
 |-  ( y = ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` w ) -> ( ( y +s 1s ) e. B <-> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` w ) +s 1s ) e. B ) )
18 17 imbi2d 
 |-  ( y = ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` w ) -> ( ( ph -> ( y +s 1s ) e. B ) <-> ( ph -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` w ) +s 1s ) e. B ) ) )
19 4 expcom 
 |-  ( y e. B -> ( ph -> ( y +s 1s ) e. B ) )
20 18 19 vtoclga 
 |-  ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` w ) e. B -> ( ph -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` w ) +s 1s ) e. B ) )
21 20 impcom 
 |-  ( ( ph /\ ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` w ) e. B ) -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` w ) +s 1s ) e. B )
22 ovex 
 |-  ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` w ) +s 1s ) e. _V
23 eqid 
 |-  ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om )
24 oveq1 
 |-  ( t = x -> ( t +s 1s ) = ( x +s 1s ) )
25 oveq1 
 |-  ( t = ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` w ) -> ( t +s 1s ) = ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` w ) +s 1s ) )
26 23 24 25 frsucmpt2 
 |-  ( ( w e. _om /\ ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` w ) +s 1s ) e. _V ) -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` suc w ) = ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` w ) +s 1s ) )
27 22 26 mpan2 
 |-  ( w e. _om -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` suc w ) = ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` w ) +s 1s ) )
28 27 eleq1d 
 |-  ( w e. _om -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` suc w ) e. B <-> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` w ) +s 1s ) e. B ) )
29 21 28 imbitrrid 
 |-  ( w e. _om -> ( ( ph /\ ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` w ) e. B ) -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` suc w ) e. B ) )
30 29 expd 
 |-  ( w e. _om -> ( ph -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` w ) e. B -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` suc w ) e. B ) ) )
31 8 10 12 15 30 finds2 
 |-  ( z e. _om -> ( ph -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` z ) e. B ) )
32 31 com12 
 |-  ( ph -> ( z e. _om -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` z ) e. B ) )
33 32 ralrimiv 
 |-  ( ph -> A. z e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` z ) e. B )
34 frfnom 
 |-  ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) Fn _om
35 ffnfv 
 |-  ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) : _om --> B <-> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) Fn _om /\ A. z e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` z ) e. B ) )
36 34 35 mpbiran 
 |-  ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) : _om --> B <-> A. z e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` z ) e. B )
37 33 36 sylibr 
 |-  ( ph -> ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) : _om --> B )
38 37 frnd 
 |-  ( ph -> ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) C_ B )
39 6 38 eqsstrd 
 |-  ( ph -> Z C_ B )