Metamath Proof Explorer

Theorem noseqinds

Description: Induction schema 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 )
noseqinds.3 
|- ( y = A -> ( ps <-> ch ) )
noseqinds.4 
|- ( y = z -> ( ps <-> th ) )
noseqinds.5 
|- ( y = ( z +s 1s ) -> ( ps <-> ta ) )
noseqinds.6 
|- ( y = B -> ( ps <-> et ) )
noseqinds.7 
|- ( ph -> ch )
noseqinds.8 
|- ( ( ph /\ z e. Z ) -> ( th -> ta ) )
Assertion noseqinds 
|- ( ( ph /\ B e. Z ) -> et )

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 noseqinds.3 
 |-  ( y = A -> ( ps <-> ch ) )
4 noseqinds.4 
 |-  ( y = z -> ( ps <-> th ) )
5 noseqinds.5 
 |-  ( y = ( z +s 1s ) -> ( ps <-> ta ) )
6 noseqinds.6 
 |-  ( y = B -> ( ps <-> et ) )
7 noseqinds.7 
 |-  ( ph -> ch )
8 noseqinds.8 
 |-  ( ( ph /\ z e. Z ) -> ( th -> ta ) )
9 1 2 noseq0 
 |-  ( ph -> A e. Z )
10 3 9 7 elrabd 
 |-  ( ph -> A e. { y e. Z | ps } )
11 1 adantr 
 |-  ( ( ph /\ z e. Z ) -> Z = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) " _om ) )
12 2 adantr 
 |-  ( ( ph /\ z e. Z ) -> A e. No )
13 simpr 
 |-  ( ( ph /\ z e. Z ) -> z e. Z )
14 11 12 13 noseqp1 
 |-  ( ( ph /\ z e. Z ) -> ( z +s 1s ) e. Z )
15 8 14 jctild 
 |-  ( ( ph /\ z e. Z ) -> ( th -> ( ( z +s 1s ) e. Z /\ ta ) ) )
16 15 expimpd 
 |-  ( ph -> ( ( z e. Z /\ th ) -> ( ( z +s 1s ) e. Z /\ ta ) ) )
17 4 elrab 
 |-  ( z e. { y e. Z | ps } <-> ( z e. Z /\ th ) )
18 5 elrab 
 |-  ( ( z +s 1s ) e. { y e. Z | ps } <-> ( ( z +s 1s ) e. Z /\ ta ) )
19 16 17 18 3imtr4g 
 |-  ( ph -> ( z e. { y e. Z | ps } -> ( z +s 1s ) e. { y e. Z | ps } ) )
20 19 imp 
 |-  ( ( ph /\ z e. { y e. Z | ps } ) -> ( z +s 1s ) e. { y e. Z | ps } )
21 1 2 10 20 noseqind 
 |-  ( ph -> Z C_ { y e. Z | ps } )
22 21 sselda 
 |-  ( ( ph /\ B e. Z ) -> B e. { y e. Z | ps } )
23 6 elrab 
 |-  ( B e. { y e. Z | ps } <-> ( B e. Z /\ et ) )
24 22 23 sylib 
 |-  ( ( ph /\ B e. Z ) -> ( B e. Z /\ et ) )
25 24 simprd 
 |-  ( ( ph /\ B e. Z ) -> et )