Metamath Proof Explorer

Theorem succlg

Description: Closure law for ordinal successor. (Contributed by RP, 8-Jan-2025)

Ref Expression
Assertion succlg 
|- ( ( A e. B /\ ( B = (/) \/ ( B = ( _om .o C ) /\ C e. ( On \ 1o ) ) ) ) -> suc A e. B )

Proof

Step Hyp Ref Expression
1 eleq2 
 |-  ( B = (/) -> ( A e. B <-> A e. (/) ) )
2 noel 
 |-  -. A e. (/)
3 2 pm2.21i 
 |-  ( A e. (/) -> suc A e. B )
4 1 3 syl6bi 
 |-  ( B = (/) -> ( A e. B -> suc A e. B ) )
5 4 com12 
 |-  ( A e. B -> ( B = (/) -> suc A e. B ) )
6 simpl 
 |-  ( ( A e. B /\ ( B = ( _om .o C ) /\ C e. ( On \ 1o ) ) ) -> A e. B )
7 eldifi 
 |-  ( C e. ( On \ 1o ) -> C e. On )
8 7 ad2antll 
 |-  ( ( A e. B /\ ( B = ( _om .o C ) /\ C e. ( On \ 1o ) ) ) -> C e. On )
9 omex 
 |-  _om e. _V
10 limom 
 |-  Lim _om
11 9 10 pm3.2i 
 |-  ( _om e. _V /\ Lim _om )
12 11 a1i 
 |-  ( ( A e. B /\ ( B = ( _om .o C ) /\ C e. ( On \ 1o ) ) ) -> ( _om e. _V /\ Lim _om ) )
13 ondif1 
 |-  ( C e. ( On \ 1o ) <-> ( C e. On /\ (/) e. C ) )
14 13 simprbi 
 |-  ( C e. ( On \ 1o ) -> (/) e. C )
15 14 ad2antll 
 |-  ( ( A e. B /\ ( B = ( _om .o C ) /\ C e. ( On \ 1o ) ) ) -> (/) e. C )
16 omlimcl2 
 |-  ( ( ( C e. On /\ ( _om e. _V /\ Lim _om ) ) /\ (/) e. C ) -> Lim ( _om .o C ) )
17 8 12 15 16 syl21anc 
 |-  ( ( A e. B /\ ( B = ( _om .o C ) /\ C e. ( On \ 1o ) ) ) -> Lim ( _om .o C ) )
18 limeq 
 |-  ( B = ( _om .o C ) -> ( Lim B <-> Lim ( _om .o C ) ) )
19 18 ad2antrl 
 |-  ( ( A e. B /\ ( B = ( _om .o C ) /\ C e. ( On \ 1o ) ) ) -> ( Lim B <-> Lim ( _om .o C ) ) )
20 17 19 mpbird 
 |-  ( ( A e. B /\ ( B = ( _om .o C ) /\ C e. ( On \ 1o ) ) ) -> Lim B )
21 limsuc 
 |-  ( Lim B -> ( A e. B <-> suc A e. B ) )
22 20 21 syl 
 |-  ( ( A e. B /\ ( B = ( _om .o C ) /\ C e. ( On \ 1o ) ) ) -> ( A e. B <-> suc A e. B ) )
23 6 22 mpbid 
 |-  ( ( A e. B /\ ( B = ( _om .o C ) /\ C e. ( On \ 1o ) ) ) -> suc A e. B )
24 23 ex 
 |-  ( A e. B -> ( ( B = ( _om .o C ) /\ C e. ( On \ 1o ) ) -> suc A e. B ) )
25 5 24 jaod 
 |-  ( A e. B -> ( ( B = (/) \/ ( B = ( _om .o C ) /\ C e. ( On \ 1o ) ) ) -> suc A e. B ) )
26 25 imp 
 |-  ( ( A e. B /\ ( B = (/) \/ ( B = ( _om .o C ) /\ C e. ( On \ 1o ) ) ) ) -> suc A e. B )