Metamath Proof Explorer

Theorem oalimcl

Description: The ordinal sum with a limit ordinal is a limit ordinal. Proposition 8.11 of TakeutiZaring p. 60. (Contributed by NM, 8-Dec-2004)

Ref Expression
Assertion oalimcl 
|- ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> Lim ( A +o B ) )

Proof

Step Hyp Ref Expression
1 limelon 
 |-  ( ( B e. C /\ Lim B ) -> B e. On )
2 oacl 
 |-  ( ( A e. On /\ B e. On ) -> ( A +o B ) e. On )
3 eloni 
 |-  ( ( A +o B ) e. On -> Ord ( A +o B ) )
4 2 3 syl 
 |-  ( ( A e. On /\ B e. On ) -> Ord ( A +o B ) )
5 1 4 sylan2 
 |-  ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> Ord ( A +o B ) )
6 0ellim 
 |-  ( Lim B -> (/) e. B )
7 n0i 
 |-  ( (/) e. B -> -. B = (/) )
8 6 7 syl 
 |-  ( Lim B -> -. B = (/) )
9 8 ad2antll 
 |-  ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> -. B = (/) )
10 oa00 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A +o B ) = (/) <-> ( A = (/) /\ B = (/) ) ) )
11 simpr 
 |-  ( ( A = (/) /\ B = (/) ) -> B = (/) )
12 10 11 syl6bi 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A +o B ) = (/) -> B = (/) ) )
13 12 con3d 
 |-  ( ( A e. On /\ B e. On ) -> ( -. B = (/) -> -. ( A +o B ) = (/) ) )
14 1 13 sylan2 
 |-  ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> ( -. B = (/) -> -. ( A +o B ) = (/) ) )
15 9 14 mpd 
 |-  ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> -. ( A +o B ) = (/) )
16 vex 
 |-  y e. _V
17 16 sucid 
 |-  y e. suc y
18 oalim 
 |-  ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> ( A +o B ) = U_ x e. B ( A +o x ) )
19 eqeq1 
 |-  ( ( A +o B ) = suc y -> ( ( A +o B ) = U_ x e. B ( A +o x ) <-> suc y = U_ x e. B ( A +o x ) ) )
20 18 19 syl5ib 
 |-  ( ( A +o B ) = suc y -> ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> suc y = U_ x e. B ( A +o x ) ) )
21 20 imp 
 |-  ( ( ( A +o B ) = suc y /\ ( A e. On /\ ( B e. C /\ Lim B ) ) ) -> suc y = U_ x e. B ( A +o x ) )
22 17 21 eleqtrid 
 |-  ( ( ( A +o B ) = suc y /\ ( A e. On /\ ( B e. C /\ Lim B ) ) ) -> y e. U_ x e. B ( A +o x ) )
23 eliun 
 |-  ( y e. U_ x e. B ( A +o x ) <-> E. x e. B y e. ( A +o x ) )
24 22 23 sylib 
 |-  ( ( ( A +o B ) = suc y /\ ( A e. On /\ ( B e. C /\ Lim B ) ) ) -> E. x e. B y e. ( A +o x ) )
25 onelon 
 |-  ( ( B e. On /\ x e. B ) -> x e. On )
26 1 25 sylan 
 |-  ( ( ( B e. C /\ Lim B ) /\ x e. B ) -> x e. On )
27 onnbtwn 
 |-  ( x e. On -> -. ( x e. B /\ B e. suc x ) )
28 imnan 
 |-  ( ( x e. B -> -. B e. suc x ) <-> -. ( x e. B /\ B e. suc x ) )
29 27 28 sylibr 
 |-  ( x e. On -> ( x e. B -> -. B e. suc x ) )
30 29 com12 
 |-  ( x e. B -> ( x e. On -> -. B e. suc x ) )
31 30 adantl 
 |-  ( ( ( B e. C /\ Lim B ) /\ x e. B ) -> ( x e. On -> -. B e. suc x ) )
32 26 31 mpd 
 |-  ( ( ( B e. C /\ Lim B ) /\ x e. B ) -> -. B e. suc x )
33 32 ad2antrl 
 |-  ( ( A e. On /\ ( ( ( B e. C /\ Lim B ) /\ x e. B ) /\ y e. ( A +o x ) ) ) -> -. B e. suc x )
34 oacl 
 |-  ( ( A e. On /\ x e. On ) -> ( A +o x ) e. On )
35 eloni 
 |-  ( ( A +o x ) e. On -> Ord ( A +o x ) )
36 ordsucelsuc 
 |-  ( Ord ( A +o x ) -> ( y e. ( A +o x ) <-> suc y e. suc ( A +o x ) ) )
37 34 35 36 3syl 
 |-  ( ( A e. On /\ x e. On ) -> ( y e. ( A +o x ) <-> suc y e. suc ( A +o x ) ) )
38 oasuc 
 |-  ( ( A e. On /\ x e. On ) -> ( A +o suc x ) = suc ( A +o x ) )
39 38 eleq2d 
 |-  ( ( A e. On /\ x e. On ) -> ( suc y e. ( A +o suc x ) <-> suc y e. suc ( A +o x ) ) )
40 37 39 bitr4d 
 |-  ( ( A e. On /\ x e. On ) -> ( y e. ( A +o x ) <-> suc y e. ( A +o suc x ) ) )
41 26 40 sylan2 
 |-  ( ( A e. On /\ ( ( B e. C /\ Lim B ) /\ x e. B ) ) -> ( y e. ( A +o x ) <-> suc y e. ( A +o suc x ) ) )
42 eleq1 
 |-  ( ( A +o B ) = suc y -> ( ( A +o B ) e. ( A +o suc x ) <-> suc y e. ( A +o suc x ) ) )
43 42 bicomd 
 |-  ( ( A +o B ) = suc y -> ( suc y e. ( A +o suc x ) <-> ( A +o B ) e. ( A +o suc x ) ) )
44 41 43 sylan9bbr 
 |-  ( ( ( A +o B ) = suc y /\ ( A e. On /\ ( ( B e. C /\ Lim B ) /\ x e. B ) ) ) -> ( y e. ( A +o x ) <-> ( A +o B ) e. ( A +o suc x ) ) )
45 1 adantr 
 |-  ( ( ( B e. C /\ Lim B ) /\ x e. B ) -> B e. On )
46 sucelon 
 |-  ( x e. On <-> suc x e. On )
47 26 46 sylib 
 |-  ( ( ( B e. C /\ Lim B ) /\ x e. B ) -> suc x e. On )
48 45 47 jca 
 |-  ( ( ( B e. C /\ Lim B ) /\ x e. B ) -> ( B e. On /\ suc x e. On ) )
49 oaord 
 |-  ( ( B e. On /\ suc x e. On /\ A e. On ) -> ( B e. suc x <-> ( A +o B ) e. ( A +o suc x ) ) )
50 49 3expa 
 |-  ( ( ( B e. On /\ suc x e. On ) /\ A e. On ) -> ( B e. suc x <-> ( A +o B ) e. ( A +o suc x ) ) )
51 48 50 sylan 
 |-  ( ( ( ( B e. C /\ Lim B ) /\ x e. B ) /\ A e. On ) -> ( B e. suc x <-> ( A +o B ) e. ( A +o suc x ) ) )
52 51 ancoms 
 |-  ( ( A e. On /\ ( ( B e. C /\ Lim B ) /\ x e. B ) ) -> ( B e. suc x <-> ( A +o B ) e. ( A +o suc x ) ) )
53 52 adantl 
 |-  ( ( ( A +o B ) = suc y /\ ( A e. On /\ ( ( B e. C /\ Lim B ) /\ x e. B ) ) ) -> ( B e. suc x <-> ( A +o B ) e. ( A +o suc x ) ) )
54 44 53 bitr4d 
 |-  ( ( ( A +o B ) = suc y /\ ( A e. On /\ ( ( B e. C /\ Lim B ) /\ x e. B ) ) ) -> ( y e. ( A +o x ) <-> B e. suc x ) )
55 54 biimpd 
 |-  ( ( ( A +o B ) = suc y /\ ( A e. On /\ ( ( B e. C /\ Lim B ) /\ x e. B ) ) ) -> ( y e. ( A +o x ) -> B e. suc x ) )
56 55 exp32 
 |-  ( ( A +o B ) = suc y -> ( A e. On -> ( ( ( B e. C /\ Lim B ) /\ x e. B ) -> ( y e. ( A +o x ) -> B e. suc x ) ) ) )
57 56 com4l 
 |-  ( A e. On -> ( ( ( B e. C /\ Lim B ) /\ x e. B ) -> ( y e. ( A +o x ) -> ( ( A +o B ) = suc y -> B e. suc x ) ) ) )
58 57 imp32 
 |-  ( ( A e. On /\ ( ( ( B e. C /\ Lim B ) /\ x e. B ) /\ y e. ( A +o x ) ) ) -> ( ( A +o B ) = suc y -> B e. suc x ) )
59 33 58 mtod 
 |-  ( ( A e. On /\ ( ( ( B e. C /\ Lim B ) /\ x e. B ) /\ y e. ( A +o x ) ) ) -> -. ( A +o B ) = suc y )
60 59 exp44 
 |-  ( A e. On -> ( ( B e. C /\ Lim B ) -> ( x e. B -> ( y e. ( A +o x ) -> -. ( A +o B ) = suc y ) ) ) )
61 60 imp 
 |-  ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> ( x e. B -> ( y e. ( A +o x ) -> -. ( A +o B ) = suc y ) ) )
62 61 rexlimdv 
 |-  ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> ( E. x e. B y e. ( A +o x ) -> -. ( A +o B ) = suc y ) )
63 62 adantl 
 |-  ( ( ( A +o B ) = suc y /\ ( A e. On /\ ( B e. C /\ Lim B ) ) ) -> ( E. x e. B y e. ( A +o x ) -> -. ( A +o B ) = suc y ) )
64 24 63 mpd 
 |-  ( ( ( A +o B ) = suc y /\ ( A e. On /\ ( B e. C /\ Lim B ) ) ) -> -. ( A +o B ) = suc y )
65 64 expcom 
 |-  ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> ( ( A +o B ) = suc y -> -. ( A +o B ) = suc y ) )
66 65 pm2.01d 
 |-  ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> -. ( A +o B ) = suc y )
67 66 adantr 
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ y e. On ) -> -. ( A +o B ) = suc y )
68 67 nrexdv 
 |-  ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> -. E. y e. On ( A +o B ) = suc y )
69 ioran 
 |-  ( -. ( ( A +o B ) = (/) \/ E. y e. On ( A +o B ) = suc y ) <-> ( -. ( A +o B ) = (/) /\ -. E. y e. On ( A +o B ) = suc y ) )
70 15 68 69 sylanbrc 
 |-  ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> -. ( ( A +o B ) = (/) \/ E. y e. On ( A +o B ) = suc y ) )
71 dflim3 
 |-  ( Lim ( A +o B ) <-> ( Ord ( A +o B ) /\ -. ( ( A +o B ) = (/) \/ E. y e. On ( A +o B ) = suc y ) ) )
72 5 70 71 sylanbrc 
 |-  ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> Lim ( A +o B ) )