Metamath Proof Explorer


Theorem omlimcl

Description: The product of any nonzero ordinal with a limit ordinal is a limit ordinal. Proposition 8.24 of TakeutiZaring p. 64. (Contributed by NM, 25-Dec-2004)

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

Proof

Step Hyp Ref Expression
1 limelon
 |-  ( ( B e. C /\ Lim B ) -> B e. On )
2 omcl
 |-  ( ( 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 5 adantr
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> Ord ( A .o B ) )
7 0ellim
 |-  ( Lim B -> (/) e. B )
8 n0i
 |-  ( (/) e. B -> -. B = (/) )
9 7 8 syl
 |-  ( Lim B -> -. B = (/) )
10 n0i
 |-  ( (/) e. A -> -. A = (/) )
11 9 10 anim12ci
 |-  ( ( Lim B /\ (/) e. A ) -> ( -. A = (/) /\ -. B = (/) ) )
12 11 adantll
 |-  ( ( ( B e. C /\ Lim B ) /\ (/) e. A ) -> ( -. A = (/) /\ -. B = (/) ) )
13 12 adantll
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> ( -. A = (/) /\ -. B = (/) ) )
14 om00
 |-  ( ( A e. On /\ B e. On ) -> ( ( A .o B ) = (/) <-> ( A = (/) \/ B = (/) ) ) )
15 14 notbid
 |-  ( ( A e. On /\ B e. On ) -> ( -. ( A .o B ) = (/) <-> -. ( A = (/) \/ B = (/) ) ) )
16 ioran
 |-  ( -. ( A = (/) \/ B = (/) ) <-> ( -. A = (/) /\ -. B = (/) ) )
17 15 16 bitrdi
 |-  ( ( A e. On /\ B e. On ) -> ( -. ( A .o B ) = (/) <-> ( -. A = (/) /\ -. B = (/) ) ) )
18 1 17 sylan2
 |-  ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> ( -. ( A .o B ) = (/) <-> ( -. A = (/) /\ -. B = (/) ) ) )
19 18 adantr
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> ( -. ( A .o B ) = (/) <-> ( -. A = (/) /\ -. B = (/) ) ) )
20 13 19 mpbird
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> -. ( A .o B ) = (/) )
21 vex
 |-  y e. _V
22 21 sucid
 |-  y e. suc y
23 omlim
 |-  ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> ( A .o B ) = U_ x e. B ( A .o x ) )
24 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 ) ) )
25 24 biimpac
 |-  ( ( ( A .o B ) = U_ x e. B ( A .o x ) /\ ( A .o B ) = suc y ) -> suc y = U_ x e. B ( A .o x ) )
26 23 25 sylan
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ ( A .o B ) = suc y ) -> suc y = U_ x e. B ( A .o x ) )
27 22 26 eleqtrid
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ ( A .o B ) = suc y ) -> y e. U_ x e. B ( A .o x ) )
28 eliun
 |-  ( y e. U_ x e. B ( A .o x ) <-> E. x e. B y e. ( A .o x ) )
29 27 28 sylib
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ ( A .o B ) = suc y ) -> E. x e. B y e. ( A .o x ) )
30 29 adantlr
 |-  ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) /\ ( A .o B ) = suc y ) -> E. x e. B y e. ( A .o x ) )
31 onelon
 |-  ( ( B e. On /\ x e. B ) -> x e. On )
32 1 31 sylan
 |-  ( ( ( B e. C /\ Lim B ) /\ x e. B ) -> x e. On )
33 onnbtwn
 |-  ( x e. On -> -. ( x e. B /\ B e. suc x ) )
34 imnan
 |-  ( ( x e. B -> -. B e. suc x ) <-> -. ( x e. B /\ B e. suc x ) )
35 33 34 sylibr
 |-  ( x e. On -> ( x e. B -> -. B e. suc x ) )
36 35 com12
 |-  ( x e. B -> ( x e. On -> -. B e. suc x ) )
37 36 adantl
 |-  ( ( ( B e. C /\ Lim B ) /\ x e. B ) -> ( x e. On -> -. B e. suc x ) )
38 32 37 mpd
 |-  ( ( ( B e. C /\ Lim B ) /\ x e. B ) -> -. B e. suc x )
39 38 ad5ant24
 |-  ( ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) /\ x e. B ) /\ y e. ( A .o x ) ) -> -. B e. suc x )
40 simpl
 |-  ( ( B e. On /\ x e. B ) -> B e. On )
41 40 31 jca
 |-  ( ( B e. On /\ x e. B ) -> ( B e. On /\ x e. On ) )
42 1 41 sylan
 |-  ( ( ( B e. C /\ Lim B ) /\ x e. B ) -> ( B e. On /\ x e. On ) )
43 42 anim2i
 |-  ( ( A e. On /\ ( ( B e. C /\ Lim B ) /\ x e. B ) ) -> ( A e. On /\ ( B e. On /\ x e. On ) ) )
44 43 anassrs
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ x e. B ) -> ( A e. On /\ ( B e. On /\ x e. On ) ) )
45 omcl
 |-  ( ( A e. On /\ x e. On ) -> ( A .o x ) e. On )
46 eloni
 |-  ( ( A .o x ) e. On -> Ord ( A .o x ) )
47 ordsucelsuc
 |-  ( Ord ( A .o x ) -> ( y e. ( A .o x ) <-> suc y e. suc ( A .o x ) ) )
48 46 47 syl
 |-  ( ( A .o x ) e. On -> ( y e. ( A .o x ) <-> suc y e. suc ( A .o x ) ) )
49 oa1suc
 |-  ( ( A .o x ) e. On -> ( ( A .o x ) +o 1o ) = suc ( A .o x ) )
50 49 eleq2d
 |-  ( ( A .o x ) e. On -> ( suc y e. ( ( A .o x ) +o 1o ) <-> suc y e. suc ( A .o x ) ) )
51 48 50 bitr4d
 |-  ( ( A .o x ) e. On -> ( y e. ( A .o x ) <-> suc y e. ( ( A .o x ) +o 1o ) ) )
52 45 51 syl
 |-  ( ( A e. On /\ x e. On ) -> ( y e. ( A .o x ) <-> suc y e. ( ( A .o x ) +o 1o ) ) )
53 52 adantr
 |-  ( ( ( A e. On /\ x e. On ) /\ (/) e. A ) -> ( y e. ( A .o x ) <-> suc y e. ( ( A .o x ) +o 1o ) ) )
54 eloni
 |-  ( A e. On -> Ord A )
55 ordgt0ge1
 |-  ( Ord A -> ( (/) e. A <-> 1o C_ A ) )
56 54 55 syl
 |-  ( A e. On -> ( (/) e. A <-> 1o C_ A ) )
57 56 adantr
 |-  ( ( A e. On /\ x e. On ) -> ( (/) e. A <-> 1o C_ A ) )
58 1on
 |-  1o e. On
59 oaword
 |-  ( ( 1o e. On /\ A e. On /\ ( A .o x ) e. On ) -> ( 1o C_ A <-> ( ( A .o x ) +o 1o ) C_ ( ( A .o x ) +o A ) ) )
60 58 59 mp3an1
 |-  ( ( A e. On /\ ( A .o x ) e. On ) -> ( 1o C_ A <-> ( ( A .o x ) +o 1o ) C_ ( ( A .o x ) +o A ) ) )
61 45 60 syldan
 |-  ( ( A e. On /\ x e. On ) -> ( 1o C_ A <-> ( ( A .o x ) +o 1o ) C_ ( ( A .o x ) +o A ) ) )
62 57 61 bitrd
 |-  ( ( A e. On /\ x e. On ) -> ( (/) e. A <-> ( ( A .o x ) +o 1o ) C_ ( ( A .o x ) +o A ) ) )
63 62 biimpa
 |-  ( ( ( A e. On /\ x e. On ) /\ (/) e. A ) -> ( ( A .o x ) +o 1o ) C_ ( ( A .o x ) +o A ) )
64 omsuc
 |-  ( ( A e. On /\ x e. On ) -> ( A .o suc x ) = ( ( A .o x ) +o A ) )
65 64 adantr
 |-  ( ( ( A e. On /\ x e. On ) /\ (/) e. A ) -> ( A .o suc x ) = ( ( A .o x ) +o A ) )
66 63 65 sseqtrrd
 |-  ( ( ( A e. On /\ x e. On ) /\ (/) e. A ) -> ( ( A .o x ) +o 1o ) C_ ( A .o suc x ) )
67 66 sseld
 |-  ( ( ( A e. On /\ x e. On ) /\ (/) e. A ) -> ( suc y e. ( ( A .o x ) +o 1o ) -> suc y e. ( A .o suc x ) ) )
68 53 67 sylbid
 |-  ( ( ( A e. On /\ x e. On ) /\ (/) e. A ) -> ( y e. ( A .o x ) -> suc y e. ( A .o suc x ) ) )
69 eleq1
 |-  ( ( A .o B ) = suc y -> ( ( A .o B ) e. ( A .o suc x ) <-> suc y e. ( A .o suc x ) ) )
70 69 biimprd
 |-  ( ( A .o B ) = suc y -> ( suc y e. ( A .o suc x ) -> ( A .o B ) e. ( A .o suc x ) ) )
71 68 70 syl9
 |-  ( ( ( A e. On /\ x e. On ) /\ (/) e. A ) -> ( ( A .o B ) = suc y -> ( y e. ( A .o x ) -> ( A .o B ) e. ( A .o suc x ) ) ) )
72 71 com23
 |-  ( ( ( A e. On /\ x e. On ) /\ (/) e. A ) -> ( y e. ( A .o x ) -> ( ( A .o B ) = suc y -> ( A .o B ) e. ( A .o suc x ) ) ) )
73 72 adantlrl
 |-  ( ( ( A e. On /\ ( B e. On /\ x e. On ) ) /\ (/) e. A ) -> ( y e. ( A .o x ) -> ( ( A .o B ) = suc y -> ( A .o B ) e. ( A .o suc x ) ) ) )
74 sucelon
 |-  ( x e. On <-> suc x e. On )
75 omord
 |-  ( ( B e. On /\ suc x e. On /\ A e. On ) -> ( ( B e. suc x /\ (/) e. A ) <-> ( A .o B ) e. ( A .o suc x ) ) )
76 simpl
 |-  ( ( B e. suc x /\ (/) e. A ) -> B e. suc x )
77 75 76 syl6bir
 |-  ( ( B e. On /\ suc x e. On /\ A e. On ) -> ( ( A .o B ) e. ( A .o suc x ) -> B e. suc x ) )
78 74 77 syl3an2b
 |-  ( ( B e. On /\ x e. On /\ A e. On ) -> ( ( A .o B ) e. ( A .o suc x ) -> B e. suc x ) )
79 78 3comr
 |-  ( ( A e. On /\ B e. On /\ x e. On ) -> ( ( A .o B ) e. ( A .o suc x ) -> B e. suc x ) )
80 79 3expb
 |-  ( ( A e. On /\ ( B e. On /\ x e. On ) ) -> ( ( A .o B ) e. ( A .o suc x ) -> B e. suc x ) )
81 80 adantr
 |-  ( ( ( A e. On /\ ( B e. On /\ x e. On ) ) /\ (/) e. A ) -> ( ( A .o B ) e. ( A .o suc x ) -> B e. suc x ) )
82 73 81 syl6d
 |-  ( ( ( A e. On /\ ( B e. On /\ x e. On ) ) /\ (/) e. A ) -> ( y e. ( A .o x ) -> ( ( A .o B ) = suc y -> B e. suc x ) ) )
83 44 82 sylan
 |-  ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ x e. B ) /\ (/) e. A ) -> ( y e. ( A .o x ) -> ( ( A .o B ) = suc y -> B e. suc x ) ) )
84 83 an32s
 |-  ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) /\ x e. B ) -> ( y e. ( A .o x ) -> ( ( A .o B ) = suc y -> B e. suc x ) ) )
85 84 imp
 |-  ( ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) /\ x e. B ) /\ y e. ( A .o x ) ) -> ( ( A .o B ) = suc y -> B e. suc x ) )
86 39 85 mtod
 |-  ( ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) /\ x e. B ) /\ y e. ( A .o x ) ) -> -. ( A .o B ) = suc y )
87 86 rexlimdva2
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> ( E. x e. B y e. ( A .o x ) -> -. ( A .o B ) = suc y ) )
88 87 adantr
 |-  ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) /\ ( A .o B ) = suc y ) -> ( E. x e. B y e. ( A .o x ) -> -. ( A .o B ) = suc y ) )
89 30 88 mpd
 |-  ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) /\ ( A .o B ) = suc y ) -> -. ( A .o B ) = suc y )
90 89 pm2.01da
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> -. ( A .o B ) = suc y )
91 90 adantr
 |-  ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) /\ y e. On ) -> -. ( A .o B ) = suc y )
92 91 nrexdv
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> -. E. y e. On ( A .o B ) = suc y )
93 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 ) )
94 20 92 93 sylanbrc
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> -. ( ( A .o B ) = (/) \/ E. y e. On ( A .o B ) = suc y ) )
95 dflim3
 |-  ( Lim ( A .o B ) <-> ( Ord ( A .o B ) /\ -. ( ( A .o B ) = (/) \/ E. y e. On ( A .o B ) = suc y ) ) )
96 6 94 95 sylanbrc
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> Lim ( A .o B ) )